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