subset-closed_closure_of Y = the_family_of (Complex_of Y) ;
hence Complex_of Y is finite-membered by MATROID0:def 6; :: thesis: verum