deffunc H₁( Element of DISJOINT_PAIRS A, Element of DISJOINT_PAIRS A) -> Element of [:(Fin A),(Fin A):] = $1 \/ $2;
set M = (DISJOINT_PAIRS A) /\ { H₁(s,t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } ;
A4: C is finite ;
A5: B is finite ;
{ H₁(s,t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } is finite from FRAENKEL:sch 22(A5, A4);
then ( (DISJOINT_PAIRS A) /\ { H₁(s,t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } c= DISJOINT_PAIRS A & (DISJOINT_PAIRS A) /\ { H₁(s,t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } is finite ) by FINSET_1:1, XBOOLE_1:17;
hence (DISJOINT_PAIRS A) /\ { (s \/ t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } is Element of Fin (DISJOINT_PAIRS A) by FINSUB_1:def 5; :: thesis: verum