let I, J be set ; :: thesis: for A being ManySortedSet of [:I,I:]

for B being ManySortedSet of [:J,J:] st A cc= B holds

~ A cc= ~ B

let A be ManySortedSet of [:I,I:]; :: thesis: for B being ManySortedSet of [:J,J:] st A cc= B holds

~ A cc= ~ B

let B be ManySortedSet of [:J,J:]; :: thesis: ( A cc= B implies ~ A cc= ~ B )

assume that

A1: [:I,I:] c= [:J,J:] and

A2: for x being set st x in [:I,I:] holds

A . x c= B . x ; :: according to ALTCAT_2:def 2 :: thesis: ~ A cc= ~ B

thus [:I,I:] c= [:J,J:] by A1; :: according to ALTCAT_2:def 2 :: thesis: for b_{1} being set holds

( not b_{1} in [:I,I:] or (~ A) . b_{1} c= (~ B) . b_{1} )

let x be set ; :: thesis: ( not x in [:I,I:] or (~ A) . x c= (~ B) . x )

assume x in [:I,I:] ; :: thesis: (~ A) . x c= (~ B) . x

then consider x1, x2 being object such that

A3: ( x1 in I & x2 in I ) and

A4: x = [x1,x2] by ZFMISC_1:def 2;

A5: [x2,x1] in [:I,I:] by A3, ZFMISC_1:def 2;

dom A = [:I,I:] by PARTFUN1:def 2;

then A6: (~ A) . (x1,x2) = A . (x2,x1) by A5, FUNCT_4:def 2;

dom B = [:J,J:] by PARTFUN1:def 2;

then (~ B) . (x1,x2) = B . (x2,x1) by A1, A5, FUNCT_4:def 2;

hence (~ A) . x c= (~ B) . x by A2, A4, A5, A6; :: thesis: verum

for B being ManySortedSet of [:J,J:] st A cc= B holds

~ A cc= ~ B

let A be ManySortedSet of [:I,I:]; :: thesis: for B being ManySortedSet of [:J,J:] st A cc= B holds

~ A cc= ~ B

let B be ManySortedSet of [:J,J:]; :: thesis: ( A cc= B implies ~ A cc= ~ B )

assume that

A1: [:I,I:] c= [:J,J:] and

A2: for x being set st x in [:I,I:] holds

A . x c= B . x ; :: according to ALTCAT_2:def 2 :: thesis: ~ A cc= ~ B

thus [:I,I:] c= [:J,J:] by A1; :: according to ALTCAT_2:def 2 :: thesis: for b

( not b

let x be set ; :: thesis: ( not x in [:I,I:] or (~ A) . x c= (~ B) . x )

assume x in [:I,I:] ; :: thesis: (~ A) . x c= (~ B) . x

then consider x1, x2 being object such that

A3: ( x1 in I & x2 in I ) and

A4: x = [x1,x2] by ZFMISC_1:def 2;

A5: [x2,x1] in [:I,I:] by A3, ZFMISC_1:def 2;

dom A = [:I,I:] by PARTFUN1:def 2;

then A6: (~ A) . (x1,x2) = A . (x2,x1) by A5, FUNCT_4:def 2;

dom B = [:J,J:] by PARTFUN1:def 2;

then (~ B) . (x1,x2) = B . (x2,x1) by A1, A5, FUNCT_4:def 2;

hence (~ A) . x c= (~ B) . x by A2, A4, A5, A6; :: thesis: verum