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

proof

thus not the topology of T is empty by TDLAT_3:def 1; :: according to PENCIL_1:def 4 :: thesis: verum

end;

for A, B being Subset of T st A is independent & B c= A holds
B is independent by TDLAT_3:17;
hence T is subset-closed by 01, M1; :: 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 & B in the_family_of T ) and
02: 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

assume B c= A ; :: thesis: contradiction
then card B c= card A by CARD_1:27;
then ( card B <= card A & 0 < 1 ) by NAT_1:40;
then (card B) + 0 < (card A) + 1 by XREAL_1:10;
hence contradiction by 02; :: thesis: verum

end;

then consider x being set such that
03: ( x in B & not x in A ) by TARSKI:def 3;
reconsider x = x as Element of T by 03;
take x ; :: thesis: ( x in B \ A & A \/ {x} in the_family_of T )
thus x in B \ A by 03, XBOOLE_0:def 5; :: thesis: A \/ {x} in the_family_of T
{x} c= the carrier of T by 03, ZFMISC_1:37;
then reconsider C = A \/ {x} as Subset of T by XBOOLE_1:8;
C is independent by TDLAT_3:17;
hence A \/ {x} in the_family_of T by Def8; :: thesis: verum