let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I st X c= Y & Y c= Z holds
X c= Z
let X, Y, Z be ManySortedSet of I; :: thesis: ( X c= Y & Y c= Z implies X c= Z )
assume that
A1: X c= Y and
A2: Y c= Z ; :: thesis: X c= Z
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( i in I implies X . i c= Z . i )
assume A3: i in I ; :: thesis: X . i c= Z . i
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in X . i or e in Z . i )
assume A4: e in X . i ; :: thesis: e in Z . i
X . i c= Y . i by A1, A3;
then A5: e in Y . i by A4;
Y . i c= Z . i by A2, A3;
hence e in Z . i by A5; :: thesis: verum