let A, B be set ; :: thesis: Fin (A /\ B) = (Fin A) /\ (Fin B)
( Fin (A /\ B) c= Fin A & Fin (A /\ B) c= Fin B ) by Th23, XBOOLE_1:17;
hence Fin (A /\ B) c= (Fin A) /\ (Fin B) by XBOOLE_1:19; :: according to XBOOLE_0:def 10 :: thesis: (Fin A) /\ (Fin B) c= Fin (A /\ B)

now

let X be set ; :: thesis: ( X in (Fin A) /\ (Fin B) implies X in Fin (A /\ B) )
assume X in (Fin A) /\ (Fin B) ; :: thesis: X in Fin (A /\ B)
then ( X in Fin A & X in Fin B ) by XBOOLE_0:def 4;
then ( X c= A & X c= B & X is finite ) by Def5;
then ( X c= A /\ B & X is finite ) by XBOOLE_1:19;
hence X in Fin (A /\ B) by Def5; :: thesis: verum

end;

hence (Fin A) /\ (Fin B) c= Fin (A /\ B) by TARSKI:def 3; :: thesis: verum