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

let X be Subset of (Sub L); :: thesis: ex_sup_of X, Sub L

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

defpred S₁[ object ] means ex R being RelStr st
( R in X & L in the InternalRel of R );
defpred S₂[ 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₂[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₁[x] ) ) from XBOOLE_0:sch 1();
A3: S c= [:Y,Y:]

proof

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

proof

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;

then A7: [: the carrier of R, the carrier of R:] c= [:Y,Y:] by ZFMISC_1:96;
x in [: the carrier of R, the carrier of R:] by A5;
hence x in [:Y,Y:] by A7; :: thesis: verum

end;

A8: S c= the InternalRel of L by A2;
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); :: 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

proof

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;

the carrier of R c= Y

proof

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;

then R is SubRelStr of A by A10, YELLOW_0:def 13;
hence b <= a by Th15; :: thesis: verum

end;

let b be Element of (Sub L); :: thesis: ( X is_<=_than b implies 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

proof

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;

Y c= the carrier of B

proof

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;

then a is SubRelStr of B by A14, YELLOW_0:def 13;
hence a <= b by Th15; :: thesis: verum

end;

hence ex_sup_of X, Sub L by YELLOW_0:15; :: thesis: verum

end;

hence Sub L is complete by YELLOW_0:53; :: thesis: verum