reconsider S = bool {0} as Subset-Family of {0} ;
take M = TopStruct(# {0},S #); :: thesis: ( M is strict & not M is empty & not M is void & M is finite & M is subset-closed & M is with_exchange_property )
thus M is strict ; :: thesis: ( not M is empty & not M is void & M is finite & M is subset-closed & M is with_exchange_property )
thus not the carrier of M is empty ; :: according to STRUCT_0:def 1 :: thesis: ( not M is void & M is finite & M is subset-closed & M is with_exchange_property )
thus not the topology of M is empty ; :: according to PENCIL_1:def 4 :: thesis: ( M is finite & M is subset-closed & M is with_exchange_property )
thus the carrier of M is finite ; :: according to STRUCT_0:def 11 :: thesis: ( M is subset-closed & M is with_exchange_property )
thus the_family_of M is subset-closed by COH_SP:2; :: according to MATROID0:def 3 :: thesis: M is with_exchange_property
let A, B be finite Subset of M; :: according to MATROID0:def 4 :: thesis: ( A in the_family_of M & B in the_family_of M & card B = (card A) + 1 implies ex e being Element of M st
( e in B \ A & A \/ {e} in the_family_of M ) )
assume A in the_family_of M ; :: thesis: ( not B in the_family_of M or not card B = (card A) + 1 or ex e being Element of M st
( e in B \ A & A \/ {e} in the_family_of M ) )
assume B in the_family_of M ; :: thesis: ( not card B = (card A) + 1 or ex e being Element of M st
( e in B \ A & A \/ {e} in the_family_of M ) )
assume A1: card B = (card A) + 1 ; :: thesis: ex e being Element of M st
( e in B \ A & A \/ {e} in the_family_of M )
reconsider e = 0 as Element of M by TARSKI:def 1;
take e ; :: thesis: ( e in B \ A & A \/ {e} in the_family_of M )
A2: bool {0} = {{},{0}} by ZFMISC_1:24;
then A3: ( B = {} or B = {0} ) by TARSKI:def 2;
A4: ( A = {} or A = {0} ) by A2, TARSKI:def 2;
then ( card A = 0 or card A = 1 ) by CARD_1:30;
hence ( e in B \ A & A \/ {e} in the_family_of M ) by A1, A4, A3; :: thesis: verum