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

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