let x be set ; :: according to MATROID0:def 5 :: thesis: ( not x in Sub_of_Fin X or x is finite )
assume x in Sub_of_Fin X ; :: thesis: x is finite
hence x is finite by COHSP_1:def 3; :: thesis: verum