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 ) ) ) :: 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 )

proof

assume A1: D is Ideal of L ; :: 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 ) )
hence for p, q being Element of L st p in D & q in D holds
p "\/" q in D by Lm1; :: thesis: for p, q being Element of L st p in D & q [= p holds
q in D
let p, q be Element of L; :: thesis: ( p in D & q [= p implies q in D )
assume ( p in D & q [= p ) ; :: thesis: q in D
then q "\/" p in D by LATTICES:def 3;
hence q in D by A1, Lm1; :: thesis: verum

end;

assume A2: ( ( 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

now

let p, q be Element of L; :: thesis: ( ( p in D & q in D ) iff p "\/" q in D )
( p [= p "\/" q & q [= q "\/" p ) by LATTICES:5;
hence ( ( p in D & q in D ) iff p "\/" q in D ) by A2; :: thesis: verum

end;

hence D is Ideal of L by Lm1; :: thesis: verum