( RelStr(# the carrier of (Sigma S),the InternalRel of (Sigma S) #) = RelStr(# the carrier of S,the InternalRel of S #) & RelStr(# the carrier of (Sigma T),the InternalRel of (Sigma T) #) = RelStr(# the carrier of T,the InternalRel of T #) ) by YELLOW_9:def 4;
then Sigma f is directed-sups-preserving Function of (Sigma S),(Sigma T) by WAYBEL21:6;
hence Sigma f is continuous by WAYBEL17:29; :: thesis: verum