let T be non empty up-complete Poset; :: thesis: for S being non empty full directed-sups-inheriting SubRelStr of T holds incl S,T is directed-sups-preserving
let S be non empty full directed-sups-inheriting SubRelStr of T; :: thesis: incl S,T is directed-sups-preserving
set f = incl S,T;
let X be Subset of S; :: according to WAYBEL_0:def 37 :: thesis: ( X is empty or not X is directed or incl S,T preserves_sup_of X )
assume A1: ( not X is empty & X is directed & ex_sup_of X,S ) ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of (incl S,T) .: X,T & "\/" ((incl S,T) .: X),T = (incl S,T) . ("\/" X,S) )
then reconsider X' = X as non empty directed Subset of T by YELLOW_2:7;
the carrier of S c= the carrier of T by YELLOW_0:def 13;
then incl S,T = id the carrier of S by YELLOW_9:def 1;
then A2: ( (incl S,T) .: X = X' & (incl S,T) . (sup X) = sup X ) by FUNCT_1:35, FUNCT_1:162;
hence ex_sup_of (incl S,T) .: X,T by WAYBEL_0:75; :: thesis: "\/" ((incl S,T) .: X),T = (incl S,T) . ("\/" X,S)
hence "\/" ((incl S,T) .: X),T = (incl S,T) . ("\/" X,S) by A1, A2, WAYBEL_0:7; :: thesis: verum