let T be non empty TopSpace; :: thesis: for B, C1, C2, D being Subset of T st B is connected & C1 is_a_component_of D & C2 is_a_component_of D & B meets C1 & B meets C2 & B c= D holds
C1 = C2
let B, C1, C2, D be Subset of T; :: thesis: ( B is connected & C1 is_a_component_of D & C2 is_a_component_of D & B meets C1 & B meets C2 & B c= D implies C1 = C2 )
assume that
A1: B is connected and
A2: ( C1 is_a_component_of D & C2 is_a_component_of D ) and
A3: B meets C1 and
A4: ( B meets C2 & B c= D ) ; :: thesis: C1 = C2
A5: B <> {} by A3, XBOOLE_1:65;
( B c= C1 & B c= C2 ) by A1, A2, A3, A4, GOBOARD9:4;
hence C1 = C2 by A2, A5, GOBOARD9:1, XBOOLE_1:68; :: thesis: verum