let L be lower-bounded up-complete LATTICE; :: thesis: for X being Subset of L holds
( X is order-generating iff for l being Element of L ex Y being Subset of X st l = "/\" Y,L )
let X be Subset of L; :: thesis: ( X is order-generating iff for l being Element of L ex Y being Subset of X st l = "/\" Y,L )
thus ( X is order-generating implies for l being Element of L ex Y being Subset of X st l = "/\" Y,L ) :: thesis: ( ( for l being Element of L ex Y being Subset of X st l = "/\" Y,L ) implies X is order-generating )

proof

assume A1: X is order-generating ; :: thesis: for l being Element of L ex Y being Subset of X st l = "/\" Y,L
let l be Element of L; :: thesis: ex Y being Subset of X st l = "/\" Y,L
for x being set st x in (uparrow l) /\ X holds
x in X by XBOOLE_0:def 4;
then reconsider Y = (uparrow l) /\ X as Subset of X by TARSKI:def 3;
l = "/\" Y,L by A1, Def5;
hence ex Y being Subset of X st l = "/\" Y,L ; :: thesis: verum

end;

thus ( ( for l being Element of L ex Y being Subset of X st l = "/\" Y,L ) implies X is order-generating ) :: thesis: verum

proof

assume A2: for l being Element of L ex Y being Subset of X st l = "/\" Y,L ; :: 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) )
consider Y being Subset of X such that
A3: l = "/\" Y,L by A2;
set S = (uparrow l) /\ X;
thus ex_inf_of (uparrow l) /\ X,L by YELLOW_0:17; :: thesis: l = inf ((uparrow l) /\ X)

now

let x be Element of L; :: thesis: ( x in (uparrow l) /\ X implies l <= x )
assume x in (uparrow l) /\ X ; :: thesis: l <= x
then ( x in uparrow l & x in X ) by XBOOLE_0:def 4;
hence l <= x by WAYBEL_0:18; :: thesis: verum

end;

then A4: l is_<=_than (uparrow l) /\ X by LATTICE3:def 8;
for b being Element of L st b is_<=_than (uparrow l) /\ X holds
b <= l

proof

let b be Element of L; :: thesis: ( b is_<=_than (uparrow l) /\ X implies b <= l )
assume A5: b is_<=_than (uparrow l) /\ X ; :: thesis: b <= l

now

let x be Element of L; :: thesis: ( x in Y implies b <= x )
assume A6: x in Y ; :: thesis: b <= x
l is_<=_than Y by A3, YELLOW_0:33;
then l <= x by A6, LATTICE3:def 8;
then x in uparrow l by WAYBEL_0:18;
then x in (uparrow l) /\ X by A6, XBOOLE_0:def 4;
hence b <= x by A5, LATTICE3:def 8; :: thesis: verum

end;

then b is_<=_than Y by LATTICE3:def 8;
hence b <= l by A3, YELLOW_0:33; :: thesis: verum

end;

hence l = inf ((uparrow l) /\ X) by A4, YELLOW_0:33; :: thesis: verum

end;