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 A1: ( Bottom T in the carrier of S & 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 A2: ex_sup_of A,T ; :: thesis: "\/" A,T in the carrier of S
then A3: sup (finsups C) = sup C by WAYBEL_0:55;
finsups C c= the carrier of S

proof

let x be set ; :: 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
A4: ( x = "\/" Y,T & 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 A5: not x in the carrier of S ; :: thesis: contradiction
then Z <> {} by A1, A4;
hence contradiction by A4, A5, 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:24;

A6: now

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;

A7: now

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

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 A2, A6, A7, WAYBEL_0:53;
hence "\/" A,T in the carrier of S by A1, A3, WAYBEL_0:def 4; :: thesis: verum