let T be complete LATTICE; :: thesis: for S being non empty full infs-inheriting SubRelStr of T holds incl (S,T) is infs-preserving
let S be non empty full infs-inheriting SubRelStr of T; :: thesis: incl (S,T) is infs-preserving
set f = incl (S,T);
let X be Subset of S; :: according to WAYBEL_0:def 32 :: thesis: incl (S,T) preserves_inf_of X
assume ex_inf_of X,S ; :: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of (incl (S,T)) .: X,T & "/\" (((incl (S,T)) .: X),T) = (incl (S,T)) . ("/\" (X,S)) )
thus ex_inf_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:92;
A3: ex_inf_of X,T by YELLOW_0:17;
A4: (incl (S,T)) . (inf X) = inf X by A1;
"/\" (X,T) in the carrier of S by A3, YELLOW_0:def 18;
hence "/\" (((incl (S,T)) .: X),T) = (incl (S,T)) . ("/\" (X,S)) by A2, A3, A4, YELLOW_0:63; :: thesis: verum