let L be Lattice; :: thesis: for X being Subset of L st ( for p, q being Element of L holds
( ( p in X & q in X ) iff p "/\" q in X ) ) holds
X is ClosedSubset of L
let X be Subset of L; :: thesis: ( ( for p, q being Element of L holds
( ( p in X & q in X ) iff p "/\" q in X ) ) implies X is ClosedSubset of L )
assume A1: for p, q being Element of L holds
( ( p in X & q in X ) iff p "/\" q in X ) ; :: thesis: X is ClosedSubset of L
let p be Element of L; :: according to LATTICE4:def 10 :: thesis: for b₁ being Element of the carrier of L holds
( not p in X or not b₁ in X or ( p "/\" b₁ in X & p "\/" b₁ in X ) )
let q be Element of L; :: thesis: ( not p in X or not q in X or ( p "/\" q in X & p "\/" q in X ) )
p "/\" (p "\/" q) = p by LATTICES:def 9;
hence ( not p in X or not q in X or ( p "/\" q in X & p "\/" q in X ) ) by A1; :: thesis: verum