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) ` & b in (L~ f) ` ) and
A4: 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:
A5: a in (LeftComp f) \/ (RightComp f) by A3, GOBRD12:11;
A6: b in (LeftComp f) \/ (RightComp f) by A3, GOBRD12:11;

per cases by A5, XBOOLE_0:def 3;

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

now

per cases by A6, 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, A4, A7; :: 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 A7; :: 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 A8: a in RightComp f ; :: thesis:

now

per cases by A6, 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, A4, A8; :: 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 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;

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 A9: ( ( 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

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

per cases by A9;

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;

thus 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

now

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

now

per cases by A9;

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

now

per cases by A1, A13, GOBOARD9:3;

suppose C = LeftComp f ; :: thesis:

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

end;

suppose C misses LeftComp f ; :: thesis:

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

end;

end;

end;

hence contradiction ; :: thesis:

end;

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

now

per cases by A1, A13, GOBOARD9:3;

suppose C = LeftComp f ; :: thesis:

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

end;

suppose C misses LeftComp f ; :: thesis:

hence contradiction by A13, A15, 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;

end;