let X be non empty TopSpace; :: thesis: for A, B being Subset of X st A is a_component & A c= B holds

A is_a_component_of B

let A, B be Subset of X; :: thesis: ( A is a_component & A c= B implies A is_a_component_of B )

assume that

A1: A is a_component and

A2: A c= B ; :: thesis: A is_a_component_of B

A3: A is connected by A1;

ex A1 being Subset of (X | B) st

( A = A1 & A1 is a_component )

A is_a_component_of B

let A, B be Subset of X; :: thesis: ( A is a_component & A c= B implies A is_a_component_of B )

assume that

A1: A is a_component and

A2: A c= B ; :: thesis: A is_a_component_of B

A3: A is connected by A1;

ex A1 being Subset of (X | B) st

( A = A1 & A1 is a_component )

proof

hence
A is_a_component_of B
by CONNSP_1:def 6; :: thesis: verum
B = [#] (X | B)
by PRE_TOPC:def 5;

then reconsider C = A as Subset of (X | B) by A2;

take A1 = C; :: thesis: ( A = A1 & A1 is a_component )

A4: for D being Subset of (X | B) st D is connected & A1 c= D holds

A1 = D

hence ( A = A1 & A1 is a_component ) by A4, CONNSP_1:def 5; :: thesis: verum

end;then reconsider C = A as Subset of (X | B) by A2;

take A1 = C; :: thesis: ( A = A1 & A1 is a_component )

A4: for D being Subset of (X | B) st D is connected & A1 c= D holds

A1 = D

proof

A1 is connected
by A3, CONNSP_1:23;
let D be Subset of (X | B); :: thesis: ( D is connected & A1 c= D implies A1 = D )

assume A5: D is connected ; :: thesis: ( not A1 c= D or A1 = D )

reconsider D1 = D as Subset of X by PRE_TOPC:11;

assume A6: A1 c= D ; :: thesis: A1 = D

D1 is connected by A5, CONNSP_1:23;

hence A1 = D by A1, A6, CONNSP_1:def 5; :: thesis: verum

end;assume A5: D is connected ; :: thesis: ( not A1 c= D or A1 = D )

reconsider D1 = D as Subset of X by PRE_TOPC:11;

assume A6: A1 c= D ; :: thesis: A1 = D

D1 is connected by A5, CONNSP_1:23;

hence A1 = D by A1, A6, CONNSP_1:def 5; :: thesis: verum

hence ( A = A1 & A1 is a_component ) by A4, CONNSP_1:def 5; :: thesis: verum