let T be lower-bounded sup-Semilattice; :: thesis: for S being non empty full join-inheriting SubRelStr of T st Bottom T in the carrier of S & S is directed-sups-inheriting holds
S is sups-inheriting
let S be non empty full join-inheriting SubRelStr of T; :: thesis: ( Bottom T in the carrier of S & S is directed-sups-inheriting implies S is sups-inheriting )
assume that
A1: Bottom T in the carrier of S and
A2: S is directed-sups-inheriting ; :: thesis: S is sups-inheriting
let A be Subset of S; :: according to YELLOW_0:def 19 :: thesis: ( not ex_sup_of A,T or "\/" (A,T) in the carrier of S )
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: "\/" (A,T) in the carrier of S
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: ( not x in finsups C or x in the carrier of S )
assume x in finsups C ; :: thesis: x in the carrier of S
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: contradiction
then Z <> {} by A1, A5;
hence contradiction by A5, A6, Th15; :: thesis: verum

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: for Y being finite Subset of C st Y <> {} holds
ex_sup_of Y,T

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

end;

A8: now :: thesis: for x being Element of T st x in finsups C holds
ex Y being finite Subset of C st
( ex_sup_of Y,T & x = "\/" (Y,T) )

let x be Element of T; :: thesis: ( x in finsups C implies ex Y being finite Subset of C st
( ex_sup_of Y,T & x = "\/" (Y,T) ) )
assume x in finsups C ; :: thesis: ex Y being finite Subset of C st
( ex_sup_of Y,T & x = "\/" (Y,T) )
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: verum

end;

now :: thesis: for Y being finite Subset of C st Y <> {} holds
"\/" (Y,T) in finsups C

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

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