let T be complete LATTICE; :: thesis: for S being non empty full sups-inheriting SubRelStr of T holds incl S,T is sups-preserving
let S be non empty full sups-inheriting SubRelStr of T; :: thesis: incl S,T is sups-preserving
set f = incl S,T;
let X be Subset of S; :: according to WAYBEL_0:def 33 :: thesis: incl S,T preserves_sup_of X
assume 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) )
thus ex_sup_of (incl S,T) .: X,T by YELLOW_0:17; :: thesis: "\/" ((incl S,T) .: X),T = (incl S,T) . ("\/" X,S)
the carrier of S c= the carrier of T by YELLOW_0:def 13;
then A1: incl S,T = id the carrier of S by YELLOW_9:def 1;
then A2: (incl S,T) .: X = X by FUNCT_1:162;
A3: ex_sup_of X,T by YELLOW_0:17;
A4: (incl S,T) . (sup X) = sup X by A1, FUNCT_1:35;
"\/" X,T in the carrier of S by A3, YELLOW_0:def 19;
hence "\/" ((incl S,T) .: X),T = (incl S,T) . ("\/" X,S) by A2, A3, A4, YELLOW_0:65; :: thesis: verum