let T be complete LATTICE; 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; incl (S,T) is sups-preserving
set f = incl (S,T);
let X be Subset of S; WAYBEL_0:def 33 incl (S,T) preserves_sup_of X
assume
ex_sup_of X,S
; WAYBEL_0:def 31 ( 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; "\/" (((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:92;
A3:
ex_sup_of X,T
by YELLOW_0:17;
A4:
(incl (S,T)) . (sup X) = sup X
by A1;
"\/" (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:64; verum