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 X = {} ; :: thesis: ( ex_inf_of f .: X,T & "/\" (f .: X),T = f . ("/\" X,S) )

then A3: ( f .: X = {} & S is upper-bounded ) by A2, RELAT_1:149, WAYBEL20:5;
hence ex_inf_of f .: X,T by A1, YELLOW_0:43; :: thesis: "/\" (f .: X),T = f . ("/\" X,S)
thus f . (inf X) = inf (f .: X) by A3, 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 ;
( dom f = the carrier of S & f . a = Top T ) by FUNCOP_1:13, FUNCOP_1:19;
then Top T in f .: X by FUNCT_1:def 12;
then ( {(Top T)} c= f .: X & f .: X c= {(Top T)} ) by FUNCOP_1:96, ZFMISC_1:37;
then ( {(Top T)} = f .: X & f . (inf X) = Top T ) by FUNCOP_1:13, XBOOLE_0:def 10;
hence ( ex_inf_of f .: X,T & "/\" (f .: X),T = f . ("/\" X,S) ) by YELLOW_0:38, YELLOW_0:39; :: thesis: verum

end;

end;