let T be discrete SubsetFamilyStr; :: thesis: ( not T is void & T is subset-closed & T is with_exchange_property )

not the topology of T is empty by TDLAT_3:def 1;

hence A1: not T is void ; :: thesis: ( T is subset-closed & T is with_exchange_property )

for A, B being Subset of T st A is independent & B c= A holds

B is independent by TDLAT_3:15;

hence T is subset-closed by A1, Th3; :: thesis: T is with_exchange_property

let A, B be finite Subset of T; :: according to MATROID0:def 4 :: thesis: ( A in the_family_of T & B in the_family_of T & card B = (card A) + 1 implies ex e being Element of T st

( e in B \ A & A \/ {e} in the_family_of T ) )

assume that

A in the_family_of T and

B in the_family_of T and

A2: card B = (card A) + 1 ; :: thesis: ex e being Element of T st

( e in B \ A & A \/ {e} in the_family_of T )

A3: x in B and

A4: not x in A ;

reconsider x = x as Element of T by A3;

{x} c= the carrier of T by A3, ZFMISC_1:31;

then reconsider C = A \/ {x} as Subset of T by XBOOLE_1:8;

take x ; :: thesis: ( x in B \ A & A \/ {x} in the_family_of T )

thus x in B \ A by A3, A4, XBOOLE_0:def 5; :: thesis: A \/ {x} in the_family_of T

C is independent by TDLAT_3:15;

hence A \/ {x} in the_family_of T ; :: thesis: verum

not the topology of T is empty by TDLAT_3:def 1;

hence A1: not T is void ; :: thesis: ( T is subset-closed & T is with_exchange_property )

for A, B being Subset of T st A is independent & B c= A holds

B is independent by TDLAT_3:15;

hence T is subset-closed by A1, Th3; :: thesis: T is with_exchange_property

let A, B be finite Subset of T; :: according to MATROID0:def 4 :: thesis: ( A in the_family_of T & B in the_family_of T & card B = (card A) + 1 implies ex e being Element of T st

( e in B \ A & A \/ {e} in the_family_of T ) )

assume that

A in the_family_of T and

B in the_family_of T and

A2: card B = (card A) + 1 ; :: thesis: ex e being Element of T st

( e in B \ A & A \/ {e} in the_family_of T )

now :: thesis: not B c= A

then consider x being object such that assume
B c= A
; :: thesis: contradiction

then Segm (card B) c= Segm (card A) by CARD_1:11;

then card B <= card A by NAT_1:39;

then (card B) + 0 < (card A) + 1 by XREAL_1:8;

hence contradiction by A2; :: thesis: verum

end;then Segm (card B) c= Segm (card A) by CARD_1:11;

then card B <= card A by NAT_1:39;

then (card B) + 0 < (card A) + 1 by XREAL_1:8;

hence contradiction by A2; :: thesis: verum

A3: x in B and

A4: not x in A ;

reconsider x = x as Element of T by A3;

{x} c= the carrier of T by A3, ZFMISC_1:31;

then reconsider C = A \/ {x} as Subset of T by XBOOLE_1:8;

take x ; :: thesis: ( x in B \ A & A \/ {x} in the_family_of T )

thus x in B \ A by A3, A4, XBOOLE_0:def 5; :: thesis: A \/ {x} in the_family_of T

C is independent by TDLAT_3:15;

hence A \/ {x} in the_family_of T ; :: thesis: verum