let IT, A, B be Element of DEDEKIND_CUTS ; :: thesis: ( IT = { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } implies IT = { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) } )
set C = { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } ;
set D = { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) } ;
A13: { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) } c= { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) }

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) } or e in { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } )
assume e in { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) } ; :: thesis: e in { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) }
then ex r, s being Element of RAT+ st
( e = r + s & r in B & s in A ) ;
hence e in { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } ; :: thesis: verum

end;

{ (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } c= { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) }

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } or e in { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) } )
assume e in { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } ; :: thesis: e in { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) }
then ex r, s being Element of RAT+ st
( e = r + s & r in A & s in B ) ;
hence e in { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) } ; :: thesis: verum

end;

hence ( IT = { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } implies IT = { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) } ) by A13; :: thesis: verum