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 :: thesis: for l1 being object st l1 in the carrier of L holds
l1 in Y
let l1 be object ; :: 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 ;
( (uparrow l) /\ Y c= Y & () /\ X c= () /\ Y ) by ;
then A4: (uparrow l) /\ X c= Y ;
l = inf (() /\ X) by A1;
hence l1 in Y by A3, A4; :: thesis: verum
end;
hence the carrier of L c= Y ; :: 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
set Y = { ("/\" (Z,L)) where Z is Subset of L : Z c= X } ;
now :: thesis: for x being object st x in { ("/\" (Z,L)) where Z is Subset of L : Z c= X } holds
x in the carrier of L
let x be object ; :: 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 ex Z being Subset of L st
( x = "/\" (Z,L) & Z c= X ) ;
hence x in the carrier of L ; :: 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 :: thesis: for x being object st x in X holds
x in Y
let x be object ; :: thesis: ( x in X implies x in Y )
assume A5: x in X ; :: thesis: x in Y
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 ;
hence x in Y by A6; :: thesis: verum
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: 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
set S = union { A where A is Subset of L : ( A c= X & "/\" (A,L) in Z ) } ;
now :: thesis: for x being object st x in union { A where A is Subset of L : ( A c= X & "/\" (A,L) in Z ) } holds
x in the carrier of L
let x be object ; :: 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
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: 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;
defpred S1[ Subset of L] means ( \$1 c= X & "/\" (\$1,L) in Z );
set N = { ("/\" (A,L)) where A is Subset of L : S1[A] } ;
now :: thesis: for x being object st x in Z holds
x in { ("/\" (A,L)) where A is Subset of L : S1[A] }
let x be object ; :: thesis: ( x in Z implies x in { ("/\" (A,L)) where A is Subset of L : S1[A] } )
assume A11: x in Z ; :: thesis: x in { ("/\" (A,L)) where A is Subset of L : S1[A] }
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 : S1[A] } by A11; :: thesis: verum
end;
then A12: Z c= { ("/\" (A,L)) where A is Subset of L : S1[A] } ;
now :: thesis: for B being set st B in { A where A is Subset of L : ( A c= X & "/\" (A,L) in Z ) } holds
B c= X
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 ex A being Subset of L st
( B = A & A c= X & "/\" (A,L) in Z ) ;
hence B c= X ; :: thesis: verum
end;
then A13: S c= X by ZFMISC_1:76;
now :: thesis: for x being object st x in { ("/\" (A,L)) where A is Subset of L : S1[A] } holds
x in Z
let x be object ; :: thesis: ( x in { ("/\" (A,L)) where A is Subset of L : S1[A] } implies x in Z )
assume x in { ("/\" (A,L)) where A is Subset of L : S1[A] } ; :: thesis: x in Z
then ex S being Subset of L st
( x = "/\" (S,L) & S c= X & "/\" (S,L) in Z ) ;
hence x in Z ; :: thesis: verum
end;
then { ("/\" (A,L)) where A is Subset of L : S1[A] } c= Z ;
then "/\" (Z,L) = "/\" ( { ("/\" (A,L)) where A is Subset of L : S1[A] } ,L) by
.= "/\" ((union { A where A is Subset of L : S1[A] } ),L) from ;
hence "/\" (Z,L) in Y by A13; :: thesis: verum
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: verum
end;
hence X is order-generating by Th15; :: thesis: verum
end;