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 Th10, 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)
let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in (Fin A) /\ (Fin B) or X in Fin (A /\ B) )
reconsider XX = X as set by TARSKI:1;
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: XX c= B by Def5;
A3: X in Fin A by A1, XBOOLE_0:def 4;
then XX c= A by Def5;
then XX c= A /\ B by A2, XBOOLE_1:19;
hence X in Fin (A /\ B) by A3, Def5; :: thesis: verum