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 A1: X in (Fin A) /\ (Fin B) ; :: thesis: X in Fin (A /\ B)
then X in Fin B by XBOOLE_0:def 4;
then A2: X c= B by Def5;
A3: X in Fin A by A1, XBOOLE_0:def 4;
then X c= A by Def5;
then X c= A /\ B by A2, XBOOLE_1:19;
hence X in Fin (A /\ B) by A3, Def5; :: thesis: verum

end;

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