bool {0 } c= bool {0 } ;
then 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 02: card B = (card A) + 1 ; :: thesis: ex e being Element of M st
( e in B \ A & A \/ {e} in the_family_of M )
bool {0 } = {{} ,{0 }} by ZFMISC_1:30;
then 04: ( ( A = {} or A = {0 } ) & ( B = {} or B = {0 } ) ) by TARSKI:def 2;
then 05: ( ( card A = 0 or card A = 1 ) & ( card B = 0 or card B = 1 ) ) by CARD_1:50;
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 )
thus ( e in B \ A & A \/ {e} in the_family_of M ) by 02, 04, 05; :: thesis: verum