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 )
now :: thesis: not B c= A
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 consider x being object such that
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