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 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;
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)
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
now :: thesis: for x being Element of L st x in Y holds
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;
then b is_<=_than Y ;
hence b <= l by A3, YELLOW_0:33; :: thesis: verum
end;
now :: thesis: for x being Element of L st x in (uparrow l) /\ X holds
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;
then l is_<=_than (uparrow l) /\ X ;
hence l = inf ((uparrow l) /\ X) by A4, YELLOW_0:33; :: thesis: verum
end;