reconsider f = the carrier of S --> (Top T) as Function of S,T ;
take f ; :: thesis: for X being finite Subset of S holds f preserves_inf_of X
let X be finite Subset of S; :: thesis: f preserves_inf_of X
assume A2: ex_inf_of X,S ; :: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of f .: X,T & "/\" (f .: X),T = f . ("/\" X,S) )

per cases ( X = {} or X <> {} ) ;

suppose A3: X = {} ; :: thesis: ( ex_inf_of f .: X,T & "/\" (f .: X),T = f . ("/\" X,S) )

then A4: f .: X = {} by RELAT_1:149;
hence ex_inf_of f .: X,T by A1, A2, A3, WAYBEL20:5, YELLOW_0:43; :: thesis: "/\" (f .: X),T = f . ("/\" X,S)
thus f . (inf X) = inf (f .: X) by A4, FUNCOP_1:13; :: thesis: verum

end;

suppose X <> {} ; :: thesis: ( ex_inf_of f .: X,T & "/\" (f .: X),T = f . ("/\" X,S) )

then reconsider A = X as non empty Subset of S ;
consider a being Element of A;
reconsider a = a as Element of S ;
A5: dom f = the carrier of S by FUNCOP_1:19;
f . a = Top T by FUNCOP_1:13;
then Top T in f .: X by A5, FUNCT_1:def 12;
then A6: {(Top T)} c= f .: X by ZFMISC_1:37;
f .: X c= {(Top T)} by FUNCOP_1:96;
then A7: {(Top T)} = f .: X by A6, XBOOLE_0:def 10;
f . (inf X) = Top T by FUNCOP_1:13;
hence ( ex_inf_of f .: X,T & "/\" (f .: X),T = f . ("/\" X,S) ) by A7, YELLOW_0:38, YELLOW_0:39; :: thesis: verum

end;

end;