let L be Lattice; :: thesis: for S being non empty Subset of L holds
( S is Ideal of L iff for p, q being Element of L holds
( ( p in S & q in S ) iff p "\/" q in S ) )
let S be non empty Subset of L; :: thesis: ( S is Ideal of L iff for p, q being Element of L holds
( ( p in S & q in S ) iff p "\/" q in S ) )
thus ( S is Ideal of L implies for p, q being Element of L holds
( ( p in S & q in S ) iff p "\/" q in S ) ) :: thesis: ( ( for p, q being Element of L holds
( ( p in S & q in S ) iff p "\/" q in S ) ) implies S is Ideal of L )

proof

assume A1: S is Ideal of L ; :: thesis: for p, q being Element of L holds
( ( p in S & q in S ) iff p "\/" q in S )
let p, q be Element of L; :: thesis: ( ( p in S & q in S ) iff p "\/" q in S )
thus ( p in S & q in S implies p "\/" q in S ) by A1, LATTICES:def 25; :: thesis: ( p "\/" q in S implies ( p in S & q in S ) )
assume A2: p "\/" q in S ; :: thesis: ( p in S & q in S )
( p [= p "\/" q & q [= p "\/" q ) by LATTICES:5;
hence ( p in S & q in S ) by A1, A2, LATTICES:def 22; :: thesis: verum

end;

assume A3: for p, q being Element of L holds
( ( p in S & q in S ) iff p "\/" q in S ) ; :: thesis: S is Ideal of L
S is initial

proof

let p, q be Element of L; :: according to LATTICES:def 22 :: thesis: ( not p [= q or not q in S or p in S )
assume that
A4: p [= q and
A5: q in S ; :: thesis: p in S
p "\/" q = q by A4, LATTICES:def 3;
hence p in S by A3, A5; :: thesis: verum

end;

hence S is Ideal of L by A3, LATTICES:def 25; :: thesis: verum