now :: thesis: for X being Subset of (Sub L) holds ex_sup_of X, Sub L

hence
Sub L is complete
by YELLOW_0:53; :: thesis: verumlet X be Subset of (Sub L); :: thesis: ex_sup_of X, Sub L

end;now :: thesis: ex a being Element of (Sub L) st

( X is_<=_than a & ( for b being Element of (Sub L) st X is_<=_than b holds

a <= b ) )

hence
ex_sup_of X, Sub L
by YELLOW_0:15; :: thesis: verum( X is_<=_than a & ( for b being Element of (Sub L) st X is_<=_than b holds

a <= b ) )

defpred S_{1}[ object ] means ex R being RelStr st

( R in X & L in the InternalRel of R );

defpred S_{2}[ object ] means ex R being RelStr st

( R in X & L in the carrier of R );

consider Y being set such that

A1: for x being object holds

( x in Y iff ( x in the carrier of L & S_{2}[x] ) )
from XBOOLE_0:sch 1();

consider S being set such that

A2: for x being object holds

( x in S iff ( x in the InternalRel of L & S_{1}[x] ) )
from XBOOLE_0:sch 1();

A3: S c= [:Y,Y:]

reconsider S = S as Relation of Y by A3;

Y c= the carrier of L by A1;

then reconsider A = RelStr(# Y,S #) as SubRelStr of L by A8, YELLOW_0:def 13;

reconsider a = A as Element of (Sub L) by Def2;

take a = a; :: thesis: ( X is_<=_than a & ( for b being Element of (Sub L) st X is_<=_than b holds

a <= b ) )

thus X is_<=_than a :: thesis: for b being Element of (Sub L) st X is_<=_than b holds

a <= b

reconsider B = b as strict SubRelStr of L by Def2;

assume A13: X is_<=_than b ; :: thesis: a <= b

A14: S c= the InternalRel of B

hence a <= b by Th15; :: thesis: verum

end;( R in X & L in the InternalRel of R );

defpred S

( R in X & L in the carrier of R );

consider Y being set such that

A1: for x being object holds

( x in Y iff ( x in the carrier of L & S

consider S being set such that

A2: for x being object holds

( x in S iff ( x in the InternalRel of L & S

A3: S c= [:Y,Y:]

proof

A8:
S c= the InternalRel of L
by A2;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in S or x in [:Y,Y:] )

assume x in S ; :: thesis: x in [:Y,Y:]

then consider R being RelStr such that

A4: R in X and

A5: x in the InternalRel of R by A2;

the carrier of R c= Y

x in [: the carrier of R, the carrier of R:] by A5;

hence x in [:Y,Y:] by A7; :: thesis: verum

end;assume x in S ; :: thesis: x in [:Y,Y:]

then consider R being RelStr such that

A4: R in X and

A5: x in the InternalRel of R by A2;

the carrier of R c= Y

proof

then A7:
[: the carrier of R, the carrier of R:] c= [:Y,Y:]
by ZFMISC_1:96;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of R or x in Y )

R is SubRelStr of L by A4, Def2;

then A6: the carrier of R c= the carrier of L by YELLOW_0:def 13;

assume x in the carrier of R ; :: thesis: x in Y

hence x in Y by A1, A4, A6; :: thesis: verum

end;R is SubRelStr of L by A4, Def2;

then A6: the carrier of R c= the carrier of L by YELLOW_0:def 13;

assume x in the carrier of R ; :: thesis: x in Y

hence x in Y by A1, A4, A6; :: thesis: verum

x in [: the carrier of R, the carrier of R:] by A5;

hence x in [:Y,Y:] by A7; :: thesis: verum

reconsider S = S as Relation of Y by A3;

Y c= the carrier of L by A1;

then reconsider A = RelStr(# Y,S #) as SubRelStr of L by A8, YELLOW_0:def 13;

reconsider a = A as Element of (Sub L) by Def2;

take a = a; :: thesis: ( X is_<=_than a & ( for b being Element of (Sub L) st X is_<=_than b holds

a <= b ) )

thus X is_<=_than a :: thesis: for b being Element of (Sub L) st X is_<=_than b holds

a <= b

proof

let b be Element of (Sub L); :: thesis: ( X is_<=_than b implies a <= b )
let b be Element of (Sub L); :: according to LATTICE3:def 9 :: thesis: ( not b in X or b <= a )

reconsider R = b as strict SubRelStr of L by Def2;

assume A9: b in X ; :: thesis: b <= a

A10: the InternalRel of R c= S

hence b <= a by Th15; :: thesis: verum

end;reconsider R = b as strict SubRelStr of L by Def2;

assume A9: b in X ; :: thesis: b <= a

A10: the InternalRel of R c= S

proof

the carrier of R c= Y
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in the InternalRel of R or [x,y] in S )

A11: the InternalRel of R c= the InternalRel of L by YELLOW_0:def 13;

assume [x,y] in the InternalRel of R ; :: thesis: [x,y] in S

hence [x,y] in S by A2, A9, A11; :: thesis: verum

end;A11: the InternalRel of R c= the InternalRel of L by YELLOW_0:def 13;

assume [x,y] in the InternalRel of R ; :: thesis: [x,y] in S

hence [x,y] in S by A2, A9, A11; :: thesis: verum

proof

then
R is SubRelStr of A
by A10, YELLOW_0:def 13;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of R or x in Y )

A12: the carrier of R c= the carrier of L by YELLOW_0:def 13;

assume x in the carrier of R ; :: thesis: x in Y

hence x in Y by A1, A9, A12; :: thesis: verum

end;A12: the carrier of R c= the carrier of L by YELLOW_0:def 13;

assume x in the carrier of R ; :: thesis: x in Y

hence x in Y by A1, A9, A12; :: thesis: verum

hence b <= a by Th15; :: thesis: verum

reconsider B = b as strict SubRelStr of L by Def2;

assume A13: X is_<=_than b ; :: thesis: a <= b

A14: S c= the InternalRel of B

proof

Y c= the carrier of B
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in S or [x,y] in the InternalRel of B )

assume [x,y] in S ; :: thesis: [x,y] in the InternalRel of B

then consider R being RelStr such that

A15: R in X and

A16: [x,y] in the InternalRel of R by A2;

reconsider c = R as Element of (Sub L) by A15;

c <= b by A13, A15;

then R is SubRelStr of B by Th15;

then the InternalRel of R c= the InternalRel of B by YELLOW_0:def 13;

hence [x,y] in the InternalRel of B by A16; :: thesis: verum

end;assume [x,y] in S ; :: thesis: [x,y] in the InternalRel of B

then consider R being RelStr such that

A15: R in X and

A16: [x,y] in the InternalRel of R by A2;

reconsider c = R as Element of (Sub L) by A15;

c <= b by A13, A15;

then R is SubRelStr of B by Th15;

then the InternalRel of R c= the InternalRel of B by YELLOW_0:def 13;

hence [x,y] in the InternalRel of B by A16; :: thesis: verum

proof

then
a is SubRelStr of B
by A14, YELLOW_0:def 13;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in the carrier of B )

assume x in Y ; :: thesis: x in the carrier of B

then consider R being RelStr such that

A17: R in X and

A18: x in the carrier of R by A1;

reconsider c = R as Element of (Sub L) by A17;

c <= b by A13, A17;

then R is SubRelStr of B by Th15;

then the carrier of R c= the carrier of B by YELLOW_0:def 13;

hence x in the carrier of B by A18; :: thesis: verum

end;assume x in Y ; :: thesis: x in the carrier of B

then consider R being RelStr such that

A17: R in X and

A18: x in the carrier of R by A1;

reconsider c = R as Element of (Sub L) by A17;

c <= b by A13, A17;

then R is SubRelStr of B by Th15;

then the carrier of R c= the carrier of B by YELLOW_0:def 13;

hence x in the carrier of B by A18; :: thesis: verum

hence a <= b by Th15; :: thesis: verum