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, Def1;
hence the carrier of S c= the carrier of S99 by XBOOLE_1:1; :: 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, Def1;
the carrier' of S9 c= the carrier' of S99 by A2, Def1;
hence the carrier' of S c= the carrier' of S99 by A3, XBOOLE_1:1; :: 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 S99 | the carrier' of S9) | the carrier' of S by RELAT_1:71
.= the Arity of S9 | the carrier' of S by A2, Def1
.= the Arity of S by A1, Def1 ; :: 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 S99 | the carrier' of S9) | the carrier' of S by RELAT_1:71
.= the ResultSort of S9 | the carrier' of S by A2, Def1
.= the ResultSort of S by A1, Def1 ; :: thesis: verum