let D, A, B be Element of DEDEKIND_CUTS ; :: thesis: ( D = { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } implies D = { (r *' s) where r, s is Element of RAT+ : ( r in B & s in A ) } )
assume A23: D = { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } ; :: thesis: D = { (r *' s) where r, s is Element of RAT+ : ( r in B & s in A ) }
now :: thesis: for e being object holds
( e in D iff e in { (r *' s) where r, s is Element of RAT+ : ( r in B & s in A ) } )
let e be object ; :: thesis: ( e in D iff e in { (r *' s) where r, s is Element of RAT+ : ( r in B & s in A ) } )
( e in D iff ex r, s being Element of RAT+ st
( e = r *' s & r in A & s in B ) ) by A23;
then ( e in D iff ex r, s being Element of RAT+ st
( e = r *' s & r in B & s in A ) ) ;
hence ( e in D iff e in { (r *' s) where r, s is Element of RAT+ : ( r in B & s in A ) } ) ; :: thesis: verum
end;
hence D = { (r *' s) where r, s is Element of RAT+ : ( r in B & s in A ) } by TARSKI:2; :: thesis: verum