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 )

( 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

thus
( ( for l being Element of L ex Y being Subset of X st l = "/\" (Y,L) ) implies X is order-generating )
:: thesis: verum
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 object 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;

hence ex Y being Subset of X st l = "/\" (Y,L) ; :: thesis: verum

end;let l be Element of L; :: thesis: ex Y being Subset of X st l = "/\" (Y,L)

for x being object 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;

hence ex Y being Subset of X st l = "/\" (Y,L) ; :: 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)

A4: for b being Element of L st b is_<=_than (uparrow l) /\ X holds

b <= l

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

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

A4: 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

hence b <= l by A3, YELLOW_0:33; :: thesis: verum

end;assume A5: b is_<=_than (uparrow l) /\ X ; :: thesis: b <= l

now :: thesis: for x being Element of L st x in Y holds

b <= x

then
b is_<=_than Y
;b <= x

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;

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; :: thesis: verum

end;assume A6: x in Y ; :: thesis: b <= x

l is_<=_than Y by A3, YELLOW_0:33;

then l <= x by A6;

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; :: thesis: verum

hence b <= l by A3, YELLOW_0:33; :: thesis: verum

now :: thesis: for x being Element of L st x in (uparrow l) /\ X holds

l <= x

then
l is_<=_than (uparrow l) /\ X
;l <= x

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 by XBOOLE_0:def 4;

hence l <= x by WAYBEL_0:18; :: thesis: verum

end;assume x in (uparrow l) /\ X ; :: thesis: l <= x

then x in uparrow l by XBOOLE_0:def 4;

hence l <= x by WAYBEL_0:18; :: thesis: verum

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