let T be lower-bounded sup-Semilattice; :: thesis:
let S be non empty full join-inheriting SubRelStr of T; :: thesis:
assume that
A1: Bottom T in the carrier of S and
A2: S is directed-sups-inheriting ; :: thesis:
let A be Subset of S; :: according to YELLOW_0:def 19 :: thesis:
the carrier of S c= the carrier of T by YELLOW_0:def 13;
then reconsider C = A as Subset of T by XBOOLE_1:1;
set F = finsups C;
assume A3: ex_sup_of A,T ; :: thesis:
then A4: sup (finsups C) = sup C by WAYBEL_0:55;
finsups C c= the carrier of S

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in finsups C ; :: thesis:
then consider Y being finite Subset of C such that
A5: x = "\/" (Y,T) and
ex_sup_of Y,T ;
reconsider Y = Y as finite Subset of T by XBOOLE_1:1;
reconsider Z = Y as finite Subset of S by XBOOLE_1:1;
assume A6: not x in the carrier of S ; :: thesis:
then Z <> {} by A1, A5;
hence contradiction by A5, A6, Th15; :: thesis:

end;

then reconsider G = finsups C as non empty Subset of S ;
reconsider G = G as non empty directed Subset of S by WAYBEL10:23;

A7: now :: thesis:

let Y be finite Subset of C; :: thesis:
Y c= the carrier of T by XBOOLE_1:1;
hence ( Y <> {} implies ex_sup_of Y,T ) by YELLOW_0:54; :: thesis:

end;

A8: now :: thesis:

let x be Element of T; :: thesis:
assume x in finsups C ; :: thesis:
then ex Y being finite Subset of C st
( x = "\/" (Y,T) & ex_sup_of Y,T ) ;
hence ex Y being finite Subset of C st
( ex_sup_of Y,T & x = "\/" (Y,T) ) ; :: thesis:

end;

now :: thesis:

let Y be finite Subset of C; :: thesis:
reconsider Z = Y as finite Subset of T by XBOOLE_1:1;
assume Y <> {} ; :: thesis:
then ex_sup_of Z,T by YELLOW_0:54;
hence "\/" (Y,T) in finsups C ; :: thesis:

end;

then ex_sup_of G,T by A3, A7, A8, WAYBEL_0:53;
hence "\/" (A,T) in the carrier of S by A2, A4; :: thesis: