A1: X is finite ;
deffunc H₁( set ) -> set = (X \ {a}) \/ {b};
deffunc H₂( set ) -> set = X \/ {a};
set FF = { H₁(w) where w is Element of X : w in X } ;
set GG = { H₂(w) where w is Element of X : w in X } ;
A2: swap (X,a,b) c= { H₁(w) where w is Element of X : w in X } \/ { H₂(w) where w is Element of X : w in X }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in swap (X,a,b) or y in { H₁(w) where w is Element of X : w in X } \/ { H₂(w) where w is Element of X : w in X } )
assume y in swap (X,a,b) ; :: thesis: y in { H₁(w) where w is Element of X : w in X } \/ { H₂(w) where w is Element of X : w in X }

per cases then ( y in { ((A \ {a}) \/ {b}) where A is Element of X : a in A } or y in { (A \/ {a}) where A is Element of X : ( not a in A & A in X ) } ) by XBOOLE_0:def 3;

suppose y in { ((A \ {a}) \/ {b}) where A is Element of X : a in A } ; :: thesis: y in { H₁(w) where w is Element of X : w in X } \/ { H₂(w) where w is Element of X : w in X }

then A3: ex A being Element of X st
( y = (A \ {a}) \/ {b} & a in A ) ;
then X <> {} by SUBSET_1:def 1;
then y in { H₁(w) where w is Element of X : w in X } by A3;
hence y in { H₁(w) where w is Element of X : w in X } \/ { H₂(w) where w is Element of X : w in X } by XBOOLE_0:def 3; :: thesis: verum

end;

suppose y in { (A \/ {a}) where A is Element of X : ( not a in A & A in X ) } ; :: thesis: y in { H₁(w) where w is Element of X : w in X } \/ { H₂(w) where w is Element of X : w in X }

then A4: ex A being Element of X st
( y = A \/ {a} & not a in A & A in X ) ;
y in { H₂(w) where w is Element of X : w in X } by A4;
hence y in { H₁(w) where w is Element of X : w in X } \/ { H₂(w) where w is Element of X : w in X } by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

A5: { H₁(w) where w is Element of X : w in X } is finite from FRAENKEL:sch 21(A1);
{ H₂(w) where w is Element of X : w in X } is finite from FRAENKEL:sch 21(A1);
hence swap (X,a,b) is finite by A5, A2; :: thesis: verum