let L be lower-bounded up-complete LATTICE; :: thesis:
let X be Subset of L; :: thesis:
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:

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

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

end;

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

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:

proof

set Y = { ("/\" (Z,L)) where Z is Subset of L : Z c= X } ;

now :: thesis:

let x be object ; :: thesis:
assume x in { ("/\" (Z,L)) where Z is Subset of L : Z c= X } ; :: thesis:
then ex Z being Subset of L st
( x = "/\" (Z,L) & Z c= X ) ;
hence x in the carrier of L ; :: thesis:

end;

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

now :: thesis:

let x be object ; :: thesis:
assume A5: x in X ; :: thesis:
then reconsider x1 = x as Element of L ;
reconsider x2 = {x1} as Subset of L ;
A6: x1 = "/\" (x2,L) by YELLOW_0:39;
{x1} c= X by A5, ZFMISC_1:31;
hence x in Y by A6; :: thesis:

end;

then A7: X c= Y ;
assume A8: 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 l being Element of L ex Z being Subset of X st l = "/\" (Z,L)

proof

let l be Element of L; :: thesis:
for Z being Subset of Y holds "/\" (Z,L) in Y

proof

let Z be Subset of Y; :: thesis:
set S = union { A where A is Subset of L : ( A c= X & "/\" (A,L) in Z ) } ;

now :: thesis:

let x be object ; :: thesis:
assume x in union { A where A is Subset of L : ( A c= X & "/\" (A,L) in Z ) } ; :: thesis:
then consider Y being set such that
A9: x in Y and
A10: Y in { A where A is Subset of L : ( A c= X & "/\" (A,L) in Z ) } by TARSKI:def 4;
ex A being Subset of L st
( Y = A & A c= X & "/\" (A,L) in Z ) by A10;
hence x in the carrier of L by A9; :: thesis:

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

let x be object ; :: thesis:
assume A11: x in Z ; :: thesis:
then x in Y ;
then ex Z being Subset of L st
( x = "/\" (Z,L) & Z c= X ) ;
hence x in { ("/\" (A,L)) where A is Subset of L : S₁[A] } by A11; :: thesis:

end;

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

now :: thesis:

let B be set ; :: thesis:
assume B in { A where A is Subset of L : ( A c= X & "/\" (A,L) in Z ) } ; :: thesis:
then ex A being Subset of L st
( B = A & A c= X & "/\" (A,L) in Z ) ;
hence B c= X ; :: thesis:

end;

then A13: S c= X by ZFMISC_1:76;

now :: thesis:

let x be object ; :: thesis:
assume x in { ("/\" (A,L)) where A is Subset of L : S₁[A] } ; :: thesis:
then ex S being Subset of L st
( x = "/\" (S,L) & S c= X & "/\" (S,L) in Z ) ;
hence x in Z ; :: thesis:

end;

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

end;

then the carrier of L = Y by A8, A7;
then l in Y ;
then ex Z being Subset of L st
( l = "/\" (Z,L) & Z c= X ) ;
hence ex Z being Subset of X st l = "/\" (Z,L) ; :: thesis:

end;

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

end;