let M be non empty compact locally_euclidean TopSpace; :: thesis: ex P being a_partition of the carrier of M st
for A being Subset of M st A in P holds
( A is open & A is a_component & ex n being Nat st M | A is non empty b3 -locally_euclidean TopSpace )
set P = { (Component_of p) where p is Point of M : verum } ;
{ (Component_of p) where p is Point of M : verum } c= bool the carrier of M
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (Component_of p) where p is Point of M : verum } or x in bool the carrier of M )
assume x in { (Component_of p) where p is Point of M : verum } ; :: thesis: x in bool the carrier of M
then ex p being Point of M st x = Component_of p ;
hence x in bool the carrier of M ; :: thesis: verum
end;
then reconsider P = { (Component_of p) where p is Point of M : verum } as Subset-Family of M ;
A1: the carrier of M c= union P
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of M or x in union P )
assume x in the carrier of M ; :: thesis: x in union P
then reconsider x = x as Point of M ;
A2: Component_of x in P ;
x in Component_of x by CONNSP_1:38;
hence x in union P by A2, TARSKI:def 4; :: thesis: verum
end;
for A being Subset of M st A in P holds
( A <> {} & ( for B being Subset of M holds
( not B in P or A = B or A misses B ) ) )
proof
let A be Subset of M; :: thesis: ( A in P implies ( A <> {} & ( for B being Subset of M holds
( not B in P or A = B or A misses B ) ) ) )
assume A in P ; :: thesis: ( A <> {} & ( for B being Subset of M holds
( not B in P or A = B or A misses B ) ) )
then consider p being Point of M such that
A3: A = Component_of p and
verum ;
thus A <> {} by A3; :: thesis: for B being Subset of M holds
( not B in P or A = B or A misses B )
let B be Subset of M; :: thesis: ( not B in P or A = B or A misses B )
assume that
A4: B in P and
A5: B <> A ; :: thesis: A misses B
A6: ex q being Point of M st B = Component_of q by A4;
assume A meets B ; :: thesis: contradiction
then consider x being object such that
A7: x in A and
A8: x in B by XBOOLE_0:3;
reconsider x = x as Point of M by A7;
Component_of p = Component_of x by CONNSP_1:42, A7, A3;
hence contradiction by CONNSP_1:42, A8, A6, A5, A3; :: thesis: verum
end;
then reconsider P = P as a_partition of the carrier of M by A1, XBOOLE_0:def 10, EQREL_1:def 4;
take P ; :: thesis: for A being Subset of M st A in P holds
( A is open & A is a_component & ex n being Nat st M | A is non empty b2 -locally_euclidean TopSpace )
let A be Subset of M; :: thesis: ( A in P implies ( A is open & A is a_component & ex n being Nat st M | A is non empty b1 -locally_euclidean TopSpace ) )
assume A in P ; :: thesis: ( A is open & A is a_component & ex n being Nat st M | A is non empty b1 -locally_euclidean TopSpace )
then ex p being Point of M st A = Component_of p ;
then A is a_component by CONNSP_1:40;
hence ( A is open & A is a_component & ex n being Nat st M | A is non empty b1 -locally_euclidean TopSpace ) by Th14; :: thesis: verum