let L be Lattice; :: thesis: for X being non empty 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 Ideal of L
let X be non empty 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 Ideal 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 Ideal of L
then X is ClosedSubset of L by Th14;
hence X is Ideal of L by A1, Def3; :: thesis: verum