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 A1: ( X c= Y & Y c= Z ) ; :: thesis: X c= Z
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( i in I implies X . i c= Z . i )
assume A2: i in I ; :: thesis: X . i c= Z . i
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in X . i or e in Z . i )
A3: ( X . i c= Y . i & Y . i c= Z . i ) by A1, A2, Def5;
assume e in X . i ; :: thesis: e in Z . i
then e in Y . i by A3;
hence e in Z . i by A3; :: thesis: verum