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 Ext (X,a,b) is empty

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

end;

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

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

end;

end;