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 ;
( (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 by XBOOLE_1:1;
l = inf ((uparrow l) /\ X) by A1, Def5;
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

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

let x be set ; :: 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 A5, ZFMISC_1:37;
hence x in Y by A6; :: thesis: verum

end;

then A7: X c= Y by TARSKI:def 3;
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: X is order-generating
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

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

end;

then A12: Z c= { ("/\" A,L) where A is Subset of L : S₁[A] } 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 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:94;

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 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 : S₁[A] } c= Z by TARSKI:def 3;
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: 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;