let L be lower-bounded up-complete LATTICE; :: thesis: for X being Subset of L holds
( X is order-generating iff for l1, l2 being Element of L st not l2 <= l1 holds
ex p being Element of L st
( p in X & l1 <= p & not l2 <= p ) )
let X be Subset of L; :: thesis: ( X is order-generating iff for l1, l2 being Element of L st not l2 <= l1 holds
ex p being Element of L st
( p in X & l1 <= p & not l2 <= p ) )
thus ( X is order-generating implies for l1, l2 being Element of L st not l2 <= l1 holds
ex p being Element of L st
( p in X & l1 <= p & not l2 <= p ) ) :: thesis: ( ( for l1, l2 being Element of L st not l2 <= l1 holds
ex p being Element of L st
( p in X & l1 <= p & not l2 <= p ) ) implies X is order-generating )

proof

assume A1: X is order-generating ; :: thesis: for l1, l2 being Element of L st not l2 <= l1 holds
ex p being Element of L st
( p in X & l1 <= p & not l2 <= p )
let l1, l2 be Element of L; :: thesis: ( not l2 <= l1 implies ex p being Element of L st
( p in X & l1 <= p & not l2 <= p ) )
consider P being Subset of X such that
A2: l1 = "/\" (P,L) by A1, Th15;
assume A3: not l2 <= l1 ; :: thesis: ex p being Element of L st
( p in X & l1 <= p & not l2 <= p )

now :: thesis: ex p being Element of L st
( p in P & not l2 <= p )

assume for p being Element of L st p in P holds
l2 <= p ; :: thesis: contradiction
then l2 is_<=_than P ;
hence contradiction by A3, A2, YELLOW_0:33; :: thesis: verum

end;

then consider p being Element of L such that
A4: ( p in P & not l2 <= p ) ;
take p ; :: thesis: ( p in X & l1 <= p & not l2 <= p )
l1 is_<=_than P by A2, YELLOW_0:33;
hence ( p in X & l1 <= p & not l2 <= p ) by A4; :: thesis: verum

end;

thus ( ( for l1, l2 being Element of L st not l2 <= l1 holds
ex p being Element of L st
( p in X & l1 <= p & not l2 <= p ) ) implies X is order-generating ) :: thesis: verum

proof

assume A5: for l1, l2 being Element of L st not l2 <= l1 holds
ex p being Element of L st
( p in X & l1 <= p & not l2 <= p ) ; :: thesis: X is order-generating
let l be Element of L; :: according to WAYBEL_6:def 5 :: thesis: ( ex_inf_of (uparrow l) /\ X,L & l = inf ((uparrow l) /\ X) )
set y = inf ((uparrow l) /\ X);
thus ex_inf_of (uparrow l) /\ X,L by YELLOW_0:17; :: thesis: l = inf ((uparrow l) /\ X)
A6: inf ((uparrow l) /\ X) is_<=_than (uparrow l) /\ X by YELLOW_0:33;

now :: thesis: not inf ((uparrow l) /\ X) <> l

l is_<=_than (uparrow l) /\ X

proof

let b be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not b in (uparrow l) /\ X or l <= b )
assume b in (uparrow l) /\ X ; :: thesis: l <= b
then b in uparrow l by XBOOLE_0:def 4;
hence l <= b by WAYBEL_0:18; :: thesis: verum

end;

then l <= inf ((uparrow l) /\ X) by YELLOW_0:33;
then A7: not inf ((uparrow l) /\ X) < l by ORDERS_2:6;
assume A8: inf ((uparrow l) /\ X) <> l ; :: thesis: contradiction

now :: thesis: contradiction

per cases ( not inf ((uparrow l) /\ X) <= l or inf ((uparrow l) /\ X) = l ) by A7, ORDERS_2:def 6;

suppose not inf ((uparrow l) /\ X) <= l ; :: thesis: contradiction

then consider p being Element of L such that
A9: p in X and
A10: l <= p and
A11: not inf ((uparrow l) /\ X) <= p by A5;
p in uparrow l by A10, WAYBEL_0:18;
then p in (uparrow l) /\ X by A9, XBOOLE_0:def 4;
hence contradiction by A6, A11; :: thesis: verum

end;

suppose inf ((uparrow l) /\ X) = l ; :: thesis: contradiction

hence contradiction by A8; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence l = inf ((uparrow l) /\ X) ; :: thesis: verum

end;