set T = the Element of X;

per cases ( a in the Element of X or not a in the Element of X ) ;

suppose a in the Element of X ; :: thesis: not swap (X,a,b) is empty

then ( the Element of X \ {a}) \/ {b} in { ((A \ {a}) \/ {b}) where A is Element of X : a in A } ;
hence not swap (X,a,b) is empty ; :: thesis: verum

end;

suppose not a in the Element of X ; :: thesis: not swap (X,a,b) is empty

then the Element of X \/ {a} in { (A \/ {a}) where A is Element of X : ( not a in A & A in X ) } ;
hence not swap (X,a,b) is empty ; :: thesis: verum

end;

end;