let x be set ; :: according to FINSET_1:def 6 :: thesis: ( not x in X /\ Y or x is finite )
assume x in X /\ Y ; :: thesis: x is finite
then x in X by XBOOLE_0:def 4;
hence x is finite ; :: thesis: verum