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 ;
then {} (subdivision (P,KX)) is simplex-like by Def20;
then {} in the topology of (subdivision (P,KX)) ;
then the topology of (subdivision (P,KX)) is with_empty_element ;
hence subdivision (P,KX) is with_empty_element ; :: 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;
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 object ; :: 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:11, XBOOLE_1:1;
A4: P .: S1 c= Y

proof

let x be object ; :: 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 object such that
y in dom P and
A5: y in S1 and
A6: P . y = x by FUNCT_1:def 6;
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 object ; :: 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 object such that
A8: y in dom P and
A9: y in S and
A10: P . y = x by A2, A3, FUNCT_1:def 6;
y in S1 by A7, A9, A10;
hence x in P .: S1 by A8, A10, FUNCT_1:def 6; :: thesis: verum

end;

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

end;

let x be set ; :: according to FINSET_1:def 6,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;
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