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 that
A1: ( not X is empty & X is directed ) and
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)) )
reconsider X9 = X as non empty directed Subset of T by A1, YELLOW_2:7;
the carrier of S c= the carrier of T by YELLOW_0:def 13;
then A2: incl (S,T) = id the carrier of S by YELLOW_9:def 1;
then A3: (incl (S,T)) .: X = X9 by FUNCT_1:92;
A4: (incl (S,T)) . (sup X) = sup X by A2;
thus ex_sup_of (incl (S,T)) .: X,T by A3, 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, A3, A4, WAYBEL_0:7; :: thesis: verum