set f = the sups-preserving Function of S,T;
take the sups-preserving Function of S,T ; :: thesis: ( the sups-preserving Function of S,T is sups-preserving & the sups-preserving Function of S,T is finite-sups-preserving )
thus ( the sups-preserving Function of S,T is sups-preserving & the sups-preserving Function of S,T is finite-sups-preserving ) ; :: thesis: verum