intro h
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
⊢ x ∉ ↑(maxInvFreeSet X) → x⁻¹ ∈ ↑(maxInvFreeSet X)
X : Type u_1
inst✝ : ProperInvolutiveInv X
x : X
h : x ∉ ↑(maxInvFreeSet X)
⊢ x⁻¹ ∈ ↑(maxInvFreeSet X)