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 )

the carrier of L = Y ) implies X is order-generating ) :: thesis: verum

( 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

thus
( ( for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" (Z,L) in Y ) holds
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

thus Y c= the carrier of L ; :: thesis: verum

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

hence
the carrier of L c= Y
; :: according to XBOOLE_0:def 10 :: thesis: Y c= the carrier of Ll1 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 & (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: verum

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

l = inf ((uparrow l) /\ X) by A1;

hence l1 in Y by A3, A4; :: thesis: verum

thus Y c= the carrier of L ; :: thesis: verum

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

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)

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

then reconsider Y = { ("/\" (Z,L)) where Z is Subset of L : Z c= X } as Subset of L by TARSKI:def 3;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;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

now :: thesis: for x being object st x in X holds

x in Y

then A7:
X c= Y
;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 A5, ZFMISC_1:31;

hence x in Y by A6; :: thesis: verum

end;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:31;

hence x in Y by A6; :: thesis: verum

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

hence
X is order-generating
by Th15; :: thesis: verum
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

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;for Z being Subset of Y holds "/\" (Z,L) in Y

proof

then
the carrier of L = Y
by A8, A7;
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 ) } ;

defpred S_{1}[ Subset of L] means ( $1 c= X & "/\" ($1,L) in Z );

set N = { ("/\" (A,L)) where A is Subset of L : S_{1}[A] } ;

_{1}[A] }
;

_{1}[A] } c= Z
;

then "/\" (Z,L) = "/\" ( { ("/\" (A,L)) where A is Subset of L : S_{1}[A] } ,L)
by A12, XBOOLE_0:def 10

.= "/\" ((union { A where A is Subset of L : S_{1}[A] } ),L)
from YELLOW_3:sch 3()
;

hence "/\" (Z,L) in Y by A13; :: thesis: verum

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

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

defpred S

set N = { ("/\" (A,L)) where A is Subset of L : S

now :: thesis: for x being object st x in Z holds

x in { ("/\" (A,L)) where A is Subset of L : S_{1}[A] }

then A12:
Z c= { ("/\" (A,L)) where A is Subset of L : Sx in { ("/\" (A,L)) where A is Subset of L : S

let x be object ; :: thesis: ( x in Z implies x in { ("/\" (A,L)) where A is Subset of L : S_{1}[A] } )

assume A11: x in Z ; :: thesis: x in { ("/\" (A,L)) where A is Subset of L : S_{1}[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_{1}[A] }
by A11; :: thesis: verum

end;assume A11: x in Z ; :: thesis: x in { ("/\" (A,L)) where A is Subset of L : S

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

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

then A13:
S c= X
by ZFMISC_1:76;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;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

now :: thesis: for x being object st x in { ("/\" (A,L)) where A is Subset of L : S_{1}[A] } holds

x in Z

then
{ ("/\" (A,L)) where A is Subset of L : Sx in Z

let x be object ; :: thesis: ( x in { ("/\" (A,L)) where A is Subset of L : S_{1}[A] } implies x in Z )

assume x in { ("/\" (A,L)) where A is Subset of L : S_{1}[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;assume x in { ("/\" (A,L)) where A is Subset of L : S

then ex S being Subset of L st

( x = "/\" (S,L) & S c= X & "/\" (S,L) in Z ) ;

hence x in Z ; :: thesis: verum

then "/\" (Z,L) = "/\" ( { ("/\" (A,L)) where A is Subset of L : S

.= "/\" ((union { A where A is Subset of L : S

hence "/\" (Z,L) in Y by A13; :: thesis: verum

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