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 )
proof
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
proof
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;
A1 is connected by A3, CONNSP_1:23;
hence ( A = A1 & A1 is a_component ) by A4, CONNSP_1:def 5; :: thesis: verum
end;
hence A is_a_component_of B by CONNSP_1:def 6; :: thesis: verum