( [#] (Complex_of Y) = X & subset-closed_closure_of Y = the_family_of TopStruct(# X,(subset-closed_closure_of Y) #) ) ;
hence ( Complex_of Y is total & Complex_of Y is subset-closed ) by Def10, MATROID0:def 3; :: thesis: verum