let a, b be set ; :: thesis:
let f be non constant standard special_circular_sequence; :: thesis:
A1: LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def 1;
A2: RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def 2;
thus ( a in (L~ f) ` & b in (L~ f) ` & ( for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not a in C or not b in C ) ) & not ( a in LeftComp f & b in RightComp f ) implies ( a in RightComp f & b in LeftComp f ) ) :: thesis:

proof

assume that
A3: a in (L~ f) ` and
A4: b in (L~ f) ` and
A5: for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not a in C or not b in C ) ; :: thesis:
A6: a in (LeftComp f) \/ (RightComp f) by A3, GOBRD12:10;
A7: b in (LeftComp f) \/ (RightComp f) by A4, GOBRD12:10;

per cases by A6, XBOOLE_0:def 3;

suppose A8: a in LeftComp f ; :: thesis:

now :: thesis:

per cases by A7, XBOOLE_0:def 3;

suppose b in LeftComp f ; :: thesis:

hence ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) ) by A1, A5, A8; :: thesis:

end;

suppose b in RightComp f ; :: thesis:

hence ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) ) by A8; :: thesis:

end;

end;

end;

hence ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) ) ; :: thesis:

end;

suppose A9: a in RightComp f ; :: thesis:

now :: thesis:

per cases by A7, XBOOLE_0:def 3;

suppose b in RightComp f ; :: thesis:

hence ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) ) by A2, A5, A9; :: thesis:

end;

suppose b in LeftComp f ; :: thesis:

hence ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) ) by A9; :: thesis:

end;

end;

end;

hence ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) ) ; :: thesis:

end;

end;

end;

thus ( ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) ) implies ( a in (L~ f) ` & b in (L~ f) ` & ( for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not a in C or not b in C ) ) ) ) :: thesis:

proof

assume A10: ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) ) ; :: thesis:
thus ( a in (L~ f) ` & b in (L~ f) ` ) :: thesis:

proof

LeftComp f c= (LeftComp f) \/ (RightComp f) by XBOOLE_1:7;
then A11: LeftComp f c= (L~ f) ` by GOBRD12:10;
RightComp f c= (LeftComp f) \/ (RightComp f) by XBOOLE_1:7;
then A12: RightComp f c= (L~ f) ` by GOBRD12:10;

per cases by A10;

suppose ( a in LeftComp f & b in RightComp f ) ; :: thesis:

hence ( a in (L~ f) ` & b in (L~ f) ` ) by A11, A12; :: thesis:

end;

suppose ( a in RightComp f & b in LeftComp f ) ; :: thesis:

hence ( a in (L~ f) ` & b in (L~ f) ` ) by A11, A12; :: thesis:

end;

end;

end;

now :: thesis:

given C being Subset of (TOP-REAL 2) such that A13: C is_a_component_of (L~ f) ` and
A14: a in C and
A15: b in C ; :: thesis:

now :: thesis:

per cases by A10;

suppose A16: ( a in LeftComp f & b in RightComp f ) ; :: thesis:

now :: thesis:

per cases by A1, A13, GOBOARD9:1;

suppose C = LeftComp f ; :: thesis:

then not LeftComp f misses RightComp f by A15, A16, XBOOLE_0:3;
hence contradiction by GOBRD14:14; :: thesis:

end;

suppose C misses LeftComp f ; :: thesis:

hence contradiction by A14, A16, XBOOLE_0:3; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

suppose A17: ( a in RightComp f & b in LeftComp f ) ; :: thesis:

now :: thesis:

per cases by A1, A13, GOBOARD9:1;

suppose C = LeftComp f ; :: thesis:

then not LeftComp f misses RightComp f by A14, A17, XBOOLE_0:3;
hence contradiction by GOBRD14:14; :: thesis:

end;

suppose C misses LeftComp f ; :: thesis:

hence contradiction by A15, A17, XBOOLE_0:3; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

hence for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not a in C or not b in C ) ; :: thesis:

end;