let T be non empty TopSpace; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: verum