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₁ being set holds
( not b₁ in [:I,I:] or (~ A) . b₁ c= (~ B) . 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