let L be Lattice; :: thesis: for D being non empty Subset of L holds
( D is Ideal of L iff ( ( for p, q being Element of L st p in D & q in D holds
p "\/" q in D ) & ( for p, q being Element of L st p in D & q [= p holds
q in D ) ) )
let D be non empty Subset of L; :: thesis: ( D is Ideal of L iff ( ( for p, q being Element of L st p in D & q in D holds
p "\/" q in D ) & ( for p, q being Element of L st p in D & q [= p holds
q in D ) ) )
thus ( D is Ideal of L implies ( ( for p, q being Element of L st p in D & q in D holds
p "\/" q in D ) & ( for p, q being Element of L st p in D & q [= p holds
q in D ) ) ) by Lm1; :: thesis: ( ( for p, q being Element of L st p in D & q in D holds
p "\/" q in D ) & ( for p, q being Element of L st p in D & q [= p holds
q in D ) implies D is Ideal of L )
assume A1: ( ( for p, q being Element of L st p in D & q in D holds
p "\/" q in D ) & ( for p, q being Element of L st p in D & q [= p holds
q in D ) ) ; :: thesis: D is Ideal of L
for p, q being Element of L holds
( ( p in D & q in D ) iff p "\/" q in D ) by A1, LATTICES:5;
hence D is Ideal of L by Lm1; :: thesis: verum