:: deftheorem defines is_rougher_than PUA2MSS1:def 13 :
for S1, S2 being ManySortedSign holds
( S1 is_rougher_than S2 iff ex f, g being Function st
( f,g form_morphism_between S2,S1 & rng f = the carrier of S1 & rng g = the carrier' of S1 ) );