let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I st X [= Y & Y [= Z holds
X [= Z
let X, Y, Z be ManySortedSet of I; :: thesis: ( X [= Y & Y [= Z implies X [= Z )
assume that
A1: X [= Y and
A2: Y [= Z ; :: thesis: X [= Z
let x be ManySortedSet of I; :: according to PBOOLE:def 11 :: thesis: ( x in X implies x in Z )
assume x in X ; :: thesis: x in Z
then x in Y by A1, Def14;
hence x in Z by A2, Def14; :: thesis: verum