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