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
thus the sups-preserving Function of S,T is sups-preserving ; :: thesis: verum