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
for p, q being Element of L st p in X & q in X holds
p "\/" q in X

proof

let p, q be Element of L; :: thesis: ( p in X & q in X implies p "\/" q in X )
p "/\" (p "\/" q) = p by LATTICES:def 9;
hence ( p in X & q in X implies p "\/" q in X ) by A1; :: thesis: verum

end;

hence X is ClosedSubset of L by A1, LATTICES:def 24, LATTICES:def 25; :: thesis: verum