set PP = subdivision P,KX;
set S = the empty c=-linear simplex-like Subset-Family of KX;
P .: the empty c=-linear simplex-like Subset-Family of KX = {} KX by RELAT_1:149;
then {} (subdivision P,KX) is simplex-like by Def20;
then {} in the topology of (subdivision P,KX) by PRE_TOPC:def 5;
then the topology of (subdivision P,KX) is with_empty_element ;
hence not subdivision P,KX is with_non-empty_elements by Def8; :: thesis: ( subdivision P,KX is subset-closed & subdivision P,KX is finite-membered )
thus subdivision P,KX is subset-closed :: thesis: subdivision P,KX is finite-membered

proof

let x be set ; :: according to CLASSES1:def 1,MATROID0:def 3 :: thesis: for b₁ being set holds
( not x in the_family_of (subdivision P,KX) or not b₁ c= x or b₁ in the_family_of (subdivision P,KX) )
let y be set ; :: thesis: ( not x in the_family_of (subdivision P,KX) or not y c= x or y in the_family_of (subdivision P,KX) )
assume that
A1: x in the_family_of (subdivision P,KX) and
A2: y c= x ; :: thesis: y in the_family_of (subdivision P,KX)
reconsider X = x, Y = y as Subset of (subdivision P,KX) by A1, A2, XBOOLE_1:1;
X is simplex-like by A1, PRE_TOPC:def 5;
then consider S being c=-linear finite simplex-like Subset-Family of KX such that
A3: X = P .: S by Def20;
set S1 = { A where A is Subset of KX : ( A in S & P . A in Y ) } ;
{ A where A is Subset of KX : ( A in S & P . A in Y ) } c= S

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { A where A is Subset of KX : ( A in S & P . A in Y ) } or x in S )
assume x in { A where A is Subset of KX : ( A in S & P . A in Y ) } ; :: thesis: x in S
then ex A being Subset of KX st
( A = x & A in S & P . A in Y ) ;
hence x in S ; :: thesis: verum

end;

then reconsider S1 = { A where A is Subset of KX : ( A in S & P . A in Y ) } as c=-linear finite simplex-like Subset-Family of KX by TOPS_2:18, XBOOLE_1:1;
A4: P .: S1 c= Y

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in P .: S1 or x in Y )
assume x in P .: S1 ; :: thesis: x in Y
then consider y being set such that
y in dom P and
A5: y in S1 and
A6: P . y = x by FUNCT_1:def 12;
ex B being Subset of KX st
( y = B & B in S & P . B in Y ) by A5;
hence x in Y by A6; :: thesis: verum

end;

Y c= P .: S1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in P .: S1 )
assume A7: x in Y ; :: thesis: x in P .: S1
then consider y being set such that
A8: y in dom P and
A9: y in S and
A10: P . y = x by A2, A3, FUNCT_1:def 12;
y in S1 by A7, A9, A10;
hence x in P .: S1 by A8, A10, FUNCT_1:def 12; :: thesis: verum

end;

then P .: S1 = Y by A4, XBOOLE_0:def 10;
then Y is simplex-like by Def20;
hence y in the_family_of (subdivision P,KX) by PRE_TOPC:def 5; :: thesis: verum

end;

let x be set ; :: according to MATROID0:def 5,MATROID0:def 6 :: thesis: ( not x in the_family_of (subdivision P,KX) or x is finite )
assume A11: x in the_family_of (subdivision P,KX) ; :: thesis: x is finite
then reconsider A = x as Subset of (subdivision P,KX) ;
A is simplex-like by A11, PRE_TOPC:def 5;
then ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S by Def20;
hence x is finite ; :: thesis: verum