let T be non empty TopSpace; for A being non empty Subset of T
for B1, B2, S being Subset of T st B1 is_a_component_of A & B2 is_a_component_of A & S is_a_component_of A & B1 \/ B2 = A & not S = B1 holds
S = B2
let A be non empty Subset of T; for B1, B2, S being Subset of T st B1 is_a_component_of A & B2 is_a_component_of A & S is_a_component_of A & B1 \/ B2 = A & not S = B1 holds
S = B2
let B1, B2, S be Subset of T; ( B1 is_a_component_of A & B2 is_a_component_of A & S is_a_component_of A & B1 \/ B2 = A & not S = B1 implies S = B2 )
assume that
A1:
B1 is_a_component_of A
and
A2:
B2 is_a_component_of A
and
A3:
S is_a_component_of A
and
A4:
B1 \/ B2 = A
; ( S = B1 or S = B2 )
S c= A
by A3, Th5;
then
S meets A
by A3, Th4, XBOOLE_1:67;
then
( S meets B1 or S meets B2 )
by A4, XBOOLE_1:70;
hence
( S = B1 or S = B2 )
by A1, A2, A3, GOBOARD9:1; verum