reconsider S = bool as Subset-Family of ;
take M = TopStruct(# ,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:
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 = by ZFMISC_1:24;
then A3: ( B = {} or B = ) by TARSKI:def 2;
A4: ( A = {} or A = ) by ;
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