P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsPrime I
⊢ x ⊓ xᶜ ∈ I
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsPrime I
⊢ x ∈ I ∨ xᶜ ∈ I
apply hI.mem_or_mem
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsPrime I
⊢ ⊥ ∈ I
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsPrime I
⊢ x ⊓ xᶜ ∈ I
rw [inf_compl_eq_bot]
no goals
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsPrime I
⊢ ⊥ ∈ I
exact I.bot_mem