A6: X is finite ;
deffunc H₁( set ) -> set = X \/ {b};
deffunc H₂( set ) -> set = X;
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 } ;
A7: Ext (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 Ext (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 Ext (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 \/ {b}) where A is Element of X : a in A } or y in { A where A is Element of X : ( not a in A & A in X ) } ) by XBOOLE_0:def 3;

suppose y in { (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 A8: ex A being Element of X st
( y = 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 A8;
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 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 A9: ex A being Element of X st
( y = A & not a in A & A in X ) ;
y in { H₂(w) where w is Element of X : w in X } by A9;
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;

A10: { H₁(w) where w is Element of X : w in X } is finite from FRAENKEL:sch 21(A6);
{ H₂(w) where w is Element of X : w in X } is finite from FRAENKEL:sch 21(A6);
hence Ext (X,a,b) is finite by A10, A7; :: thesis: verum