let S be non empty RelStr ; :: thesis: for T being non empty reflexive antisymmetric upper-bounded RelStr holds S --> (Top T) is infs-preserving
let T be non empty reflexive antisymmetric upper-bounded RelStr ; :: thesis: S --> (Top T) is infs-preserving
let X be Subset of S; :: according to WAYBEL_0:def 32 :: thesis: S --> (Top T) preserves_inf_of X
assume ex_inf_of X,S ; :: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of (S --> (Top T)) .: X,T & "/\" ((S --> (Top T)) .: X),T = (S --> (Top T)) . ("/\" X,S) )
set t = Top T;
set f = the carrier of S --> (Top T);
A1: S --> (Top T) = the carrier of S --> (Top T) ;
A2: (the carrier of S --> (Top T)) . (inf X) = Top T by FUNCOP_1:13;
(S --> (Top T)) .: X c= {(Top T)} by A1, FUNCOP_1:96;
then ( (S --> (Top T)) .: X = {(Top T)} or (S --> (Top T)) .: X = {} ) by ZFMISC_1:39;
hence ( ex_inf_of (S --> (Top T)) .: X,T & "/\" ((S --> (Top T)) .: X),T = (S --> (Top T)) . ("/\" X,S) ) by A1, A2, YELLOW_0:38, YELLOW_0:39, YELLOW_0:43; :: thesis: verum