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 and
A3: C2 is_a_component_of D and
A4: B meets C1 and
A5: B meets C2 and
A6: B c= D ; :: thesis: C1 = C2
A7: B c= C1 by A1, A2, A4, A6, GOBOARD9:6;
A8: B c= C2 by A1, A3, A5, A6, GOBOARD9:6;
B <> {} by A4, XBOOLE_1:65;
hence C1 = C2 by A2, A3, A7, A8, GOBOARD9:3, XBOOLE_1:68; :: thesis: verum