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 ;
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 ;
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:
let l be Element of L; :: according to WAYBEL_6:def 5 :: thesis: ( ex_inf_of () /\ X,L & l = inf (() /\ X) )
set y = inf (() /\ X);
thus ex_inf_of () /\ X,L by YELLOW_0:17; :: thesis: l = inf (() /\ X)
A6: inf (() /\ X) is_<=_than () /\ X by YELLOW_0:33;
now :: thesis: not inf (() /\ X) <> l
l is_<=_than () /\ X
proof
let b be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not b in () /\ X or l <= b )
assume b in () /\ 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 (() /\ X) by YELLOW_0:33;
then A7: not inf (() /\ X) < l by ORDERS_2:6;
assume A8: inf (() /\ X) <> l ; :: thesis: contradiction
now :: thesis: contradiction
per cases ( not inf (() /\ X) <= l or inf (() /\ X) = l ) by ;
suppose not inf (() /\ 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 (() /\ X) <= p by A5;
p in uparrow l by ;
then p in () /\ X by ;
hence contradiction by A6, A11; :: thesis: verum
end;
suppose inf (() /\ X) = l ; :: thesis: contradiction
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
hence l = inf (() /\ X) ; :: thesis: verum
end;