let A be set ; :: thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) holds B ^ C = C ^ B
let B, C be Element of Fin (DISJOINT_PAIRS A); :: thesis: B ^ C = C ^ B
deffunc H₁( Element of DISJOINT_PAIRS A, Element of DISJOINT_PAIRS A) -> Element of [:(Fin A),(Fin A):] = $1 \/ $2;
defpred S₁[ set , set ] means ( $1 in B & $2 in C );
defpred S₂[ set , set ] means ( $2 in C & $1 in B );
set X1 = { H₁(s,t) where s, t is Element of DISJOINT_PAIRS A : S₁[s,t] } ;
set X2 = { H₁(t,s) where s, t is Element of DISJOINT_PAIRS A : S₂[s,t] } ;
A1: for s, t being Element of DISJOINT_PAIRS A holds H₁(s,t) = H₁(t,s) ;

A2: now :: thesis: for x being object holds
( x in { H₁(t,s) where s, t is Element of DISJOINT_PAIRS A : S₂[s,t] } iff x in { (t \/ s) where t, s is Element of DISJOINT_PAIRS A : ( t in C & s in B ) } )

let x be object ; :: thesis: ( x in { H₁(t,s) where s, t is Element of DISJOINT_PAIRS A : S₂[s,t] } iff x in { (t \/ s) where t, s is Element of DISJOINT_PAIRS A : ( t in C & s in B ) } )
( x in { H₁(t,s) where s, t is Element of DISJOINT_PAIRS A : S₂[s,t] } iff ex s, t being Element of DISJOINT_PAIRS A st
( x = t \/ s & t in C & s in B ) ) ;
then ( x in { H₁(t,s) where s, t is Element of DISJOINT_PAIRS A : S₂[s,t] } iff ex t, s being Element of DISJOINT_PAIRS A st
( x = t \/ s & t in C & s in B ) ) ;
hence ( x in { H₁(t,s) where s, t is Element of DISJOINT_PAIRS A : S₂[s,t] } iff x in { (t \/ s) where t, s is Element of DISJOINT_PAIRS A : ( t in C & s in B ) } ) ; :: thesis: verum

end;

A3: for s, t being Element of DISJOINT_PAIRS A holds
( S₁[s,t] iff S₂[s,t] ) ;
{ H₁(s,t) where s, t is Element of DISJOINT_PAIRS A : S₁[s,t] } = { H₁(t,s) where s, t is Element of DISJOINT_PAIRS A : S₂[s,t] } from FRAENKEL:sch 8(A3, A1);
hence B ^ C = C ^ B by A2, TARSKI:2; :: thesis: verum