let f be non constant standard special_circular_sequence; :: thesis: for a, b, c being set st a in (L~ f) ` & b in (L~ f) ` & c 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 ) ) & ( for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not b in C or not c in C ) ) holds
ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C )
let a, b, c be set ; :: thesis: ( a in (L~ f) ` & b in (L~ f) ` & c 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 ) ) & ( for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not b in C or not c in C ) ) implies ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C ) )
assume that
A1: ( a in (L~ f) ` & b in (L~ f) ` & c in (L~ f) ` ) and
A2: 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 ) and
A3: for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not b in C or not c in C ) ; :: thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C )
A4: LeftComp f is_a_component_of (L~ f) ` by GOBOARD9:def 1;
A5: RightComp f is_a_component_of (L~ f) ` by GOBOARD9:def 2;

per cases ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) ) by A1, A2, Th16;

suppose A6: ( a in LeftComp f & b in RightComp f ) ; :: thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C )

now

per cases ( ( b in LeftComp f & c in RightComp f ) or ( b in RightComp f & c in LeftComp f ) ) by A1, A3, Th16;

suppose ( b in LeftComp f & c in RightComp f ) ; :: thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C )

then LeftComp f meets RightComp f by A6, XBOOLE_0:3;
hence ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C ) by GOBRD14:24; :: thesis: verum

end;

suppose ( b in RightComp f & c in LeftComp f ) ; :: thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C )

hence ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C ) by A4, A6; :: thesis: verum

end;

end;

end;

hence ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C ) ; :: thesis: verum

end;

suppose A7: ( a in RightComp f & b in LeftComp f ) ; :: thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C )

now

per cases ( ( b in RightComp f & c in LeftComp f ) or ( b in LeftComp f & c in RightComp f ) ) by A1, A3, Th16;

suppose ( b in RightComp f & c in LeftComp f ) ; :: thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C )

then LeftComp f meets RightComp f by A7, XBOOLE_0:3;
hence ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C ) by GOBRD14:24; :: thesis: verum

end;

suppose ( b in LeftComp f & c in RightComp f ) ; :: thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C )

hence ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C ) by A5, A7; :: thesis: verum

end;

end;

end;

hence ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & a in C & c in C ) ; :: thesis: verum

end;

end;