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 )

ex p being Element of L st

( p in X & l1 <= p & not l2 <= p ) ) implies X is order-generating ) :: thesis: verum

( 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

thus
( ( for l1, l2 being Element of L st not l2 <= l1 holds
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 )

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

then consider p being Element of L such that ( 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;l2 <= p ; :: thesis: contradiction

then l2 is_<=_than P ;

hence contradiction by A3, A2, YELLOW_0:33; :: thesis: verum

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

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;

end;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

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

then A7: not inf ((uparrow l) /\ X) < l by ORDERS_2:6;

assume A8: inf ((uparrow l) /\ X) <> l ; :: thesis: contradiction

end;proof

then
l <= inf ((uparrow l) /\ X)
by YELLOW_0:33;
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;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

then A7: not inf ((uparrow l) /\ X) < l by ORDERS_2:6;

assume A8: inf ((uparrow l) /\ X) <> l ; :: thesis: contradiction

now :: thesis: contradictionend;

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

end;

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;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