let I, J be set ; 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:]; for B being ManySortedSet of [:J,J:] st A cc= B holds
~ A cc= ~ B
let B be ManySortedSet of [:J,J:]; ( 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
; ALTCAT_2:def 2 ~ A cc= ~ B
thus
[:I,I:] c= [:J,J:]
by A1; ALTCAT_2:def 2 for b1 being set holds
( not b1 in [:I,I:] or (~ A) . b1 c= (~ B) . b1 )
let x be set ; ( not x in [:I,I:] or (~ A) . x c= (~ B) . x )
assume
x in [:I,I:]
; (~ 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; verum