let T be complete LATTICE; :: thesis: for S being non empty full filtered-infs-inheriting SubRelStr of T holds incl S,T is filtered-infs-preserving
let S be non empty full filtered-infs-inheriting SubRelStr of T; :: thesis: incl S,T is filtered-infs-preserving
set f = incl S,T;
let X be Subset of S; :: according to WAYBEL_0:def 36 :: thesis: ( X is empty or not X is filtered or incl S,T preserves_inf_of X )
assume A1: ( not X is empty & X is filtered & 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 incl S,T = id the carrier of S by YELLOW_9:def 1;
then ( (incl S,T) .: X = X & ex_inf_of X,T & (incl S,T) . (inf X) = inf X ) by FUNCT_1:35, FUNCT_1:162, YELLOW_0:17;
hence "/\" ((incl S,T) .: X),T = (incl S,T) . ("/\" X,S) by A1, WAYBEL_0:6; :: thesis: verum