let S, S9, S99 be non empty ManySortedSign ; :: thesis: ( S <= S9 & S9 <= S99 implies S <= S99 )
assume that
A1: S <= S9 and
A2: S9 <= S99 ; :: thesis: S <= S99
( the carrier of S c= the carrier of S9 & the carrier of S9 c= the carrier of S99 ) by A1, A2;
hence the carrier of S c= the carrier of S99 ; :: according to MSUHOM_1:def 1 :: thesis: ( the carrier' of S c= the carrier' of S99 & the Arity of S99 | the carrier' of S = the Arity of S & the ResultSort of S99 | the carrier' of S = the ResultSort of S )
A3: the carrier' of S c= the carrier' of S9 by A1;
the carrier' of S9 c= the carrier' of S99 by A2;
hence the carrier' of S c= the carrier' of S99 by A3; :: thesis: ( the Arity of S99 | the carrier' of S = the Arity of S & the ResultSort of S99 | the carrier' of S = the ResultSort of S )
thus the Arity of S99 | the carrier' of S = the Arity of S99 | ( the carrier' of S9 /\ the carrier' of S) by A3, XBOOLE_1:28
.= the Arity of S by A1, A2, RELAT_1:71 ; :: thesis: the ResultSort of S99 | the carrier' of S = the ResultSort of S
thus the ResultSort of S99 | the carrier' of S = the ResultSort of S99 | ( the carrier' of S9 /\ the carrier' of S) by A3, XBOOLE_1:28
.= the ResultSort of S by A1, A2, RELAT_1:71 ; :: thesis: verum