let L be lower-bounded up-complete LATTICE; :: thesis: for X being Subset of L holds
( X is order-generating iff for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" Z,L in Y ) holds
the carrier of L = Y )
let X be Subset of L; :: thesis: ( X is order-generating iff for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" Z,L in Y ) holds
the carrier of L = Y )
thus ( X is order-generating implies for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" Z,L in Y ) holds
the carrier of L = Y ) :: thesis: ( ( for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" Z,L in Y ) holds
the carrier of L = Y ) implies X is order-generating )

proof

assume A1: X is order-generating ; :: thesis: for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" Z,L in Y ) holds
the carrier of L = Y
let Y be Subset of L; :: thesis: ( X c= Y & ( for Z being Subset of Y holds "/\" Z,L in Y ) implies the carrier of L = Y )
assume that
A2: X c= Y and
A3: for Z being Subset of Y holds "/\" Z,L in Y ; :: thesis: the carrier of L = Y

now

let l1 be set ; :: thesis: ( l1 in the carrier of L implies l1 in Y )
assume l1 in the carrier of L ; :: thesis: l1 in Y
then reconsider l = l1 as Element of L ;
A4: l = inf ((uparrow l) /\ X) by A1, Def5;
A5: (uparrow l) /\ Y c= Y by XBOOLE_1:17;
(uparrow l) /\ X c= (uparrow l) /\ Y by A2, XBOOLE_1:26;
then (uparrow l) /\ X c= Y by A5, XBOOLE_1:1;
hence l1 in Y by A3, A4; :: thesis: verum

end;

hence the carrier of L c= Y by TARSKI:def 3; :: according to XBOOLE_0:def 10 :: thesis: Y c= the carrier of L
thus Y c= the carrier of L ; :: thesis: verum

end;

thus ( ( for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" Z,L in Y ) holds
the carrier of L = Y ) implies X is order-generating ) :: thesis: verum

proof

assume A6: for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" Z,L in Y ) holds
the carrier of L = Y ; :: thesis: X is order-generating
set Y = { ("/\" Z,L) where Z is Subset of L : Z c= X } ;

now

let x be set ; :: thesis: ( x in { ("/\" Z,L) where Z is Subset of L : Z c= X } implies x in the carrier of L )
assume x in { ("/\" Z,L) where Z is Subset of L : Z c= X } ; :: thesis: x in the carrier of L
then consider Z being Subset of L such that
A7: ( x = "/\" Z,L & Z c= X ) ;
thus x in the carrier of L by A7; :: thesis: verum

end;

then reconsider Y = { ("/\" Z,L) where Z is Subset of L : Z c= X } as Subset of L by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in X implies x in Y )
assume A8: x in X ; :: thesis: x in Y
then reconsider x1 = x as Element of L ;
A9: {x1} c= X by A8, ZFMISC_1:37;
reconsider x2 = {x1} as Subset of L ;
x1 = "/\" x2,L by YELLOW_0:39;
hence x in Y by A9; :: thesis: verum

end;

then A10: X c= Y by TARSKI:def 3;
for l being Element of L ex Z being Subset of X st l = "/\" Z,L

proof

let l be Element of L; :: thesis: ex Z being Subset of X st l = "/\" Z,L
for Z being Subset of Y holds "/\" Z,L in Y

proof

let Z be Subset of Y; :: thesis: "/\" Z,L in Y
defpred S₁[ Subset of L] means ( $1 c= X & "/\" $1,L in Z );
set N = { ("/\" A,L) where A is Subset of L : S₁[A] } ;

now

let x be set ; :: thesis: ( x in Z implies x in { ("/\" A,L) where A is Subset of L : S₁[A] } )
assume A11: x in Z ; :: thesis: x in { ("/\" A,L) where A is Subset of L : S₁[A] }
then x in Y ;
then consider Z being Subset of L such that
A12: ( x = "/\" Z,L & Z c= X ) ;
thus x in { ("/\" A,L) where A is Subset of L : S₁[A] } by A11, A12; :: thesis: verum

end;

then A13: Z c= { ("/\" A,L) where A is Subset of L : S₁[A] } by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in { ("/\" A,L) where A is Subset of L : S₁[A] } implies x in Z )
assume x in { ("/\" A,L) where A is Subset of L : S₁[A] } ; :: thesis: x in Z
then consider S being Subset of L such that
A14: ( x = "/\" S,L & S c= X & "/\" S,L in Z ) ;
thus x in Z by A14; :: thesis: verum

end;

then { ("/\" A,L) where A is Subset of L : S₁[A] } c= Z by TARSKI:def 3;
then A15: "/\" Z,L = "/\" { ("/\" A,L) where A is Subset of L : S₁[A] } ,L by A13, XBOOLE_0:def 10
.= "/\" (union { A where A is Subset of L : S₁[A] } ),L from YELLOW_3:sch 3() ;
set S = union { A where A is Subset of L : ( A c= X & "/\" A,L in Z ) } ;

now

let x be set ; :: thesis: ( x in union { A where A is Subset of L : ( A c= X & "/\" A,L in Z ) } implies x in the carrier of L )
assume x in union { A where A is Subset of L : ( A c= X & "/\" A,L in Z ) } ; :: thesis: x in the carrier of L
then consider Y being set such that
A16: x in Y and
A17: Y in { A where A is Subset of L : ( A c= X & "/\" A,L in Z ) } by TARSKI:def 4;
consider A being Subset of L such that
A18: ( Y = A & A c= X & "/\" A,L in Z ) by A17;
thus x in the carrier of L by A16, A18; :: thesis: verum

end;

then reconsider S = union { A where A is Subset of L : ( A c= X & "/\" A,L in Z ) } as Subset of L by TARSKI:def 3;

now

let B be set ; :: thesis: ( B in { A where A is Subset of L : ( A c= X & "/\" A,L in Z ) } implies B c= X )
assume B in { A where A is Subset of L : ( A c= X & "/\" A,L in Z ) } ; :: thesis: B c= X
then consider A being Subset of L such that
A19: ( B = A & A c= X & "/\" A,L in Z ) ;
thus B c= X by A19; :: thesis: verum

end;

then S c= X by ZFMISC_1:94;
hence "/\" Z,L in Y by A15; :: thesis: verum

end;

then the carrier of L = Y by A6, A10;
then l in Y ;
then consider Z being Subset of L such that
A20: ( l = "/\" Z,L & Z c= X ) ;
thus ex Z being Subset of X st l = "/\" Z,L by A20; :: thesis: verum

end;

hence X is order-generating by Th15; :: thesis: verum

end;