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 = {} ;
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:7; :: 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 ;
set a = the Element of A;
reconsider a = the Element of A as Element of S ;
A5: dom f = the carrier of S by FUNCOP_1:13;
f . a = Top T by FUNCOP_1:7;
then Top T in f .: X by A5, FUNCT_1:def 6;
then A6: {(Top T)} c= f .: X by ZFMISC_1:31;
f .: X c= {(Top T)} by FUNCOP_1:81;
then A7: {(Top T)} = f .: X by A6;
f . (inf X) = Top T by FUNCOP_1:7;
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;