let f be non constant standard special_circular_sequence; :: thesis: for a, b, c being set st ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & a in C & b in C ) & ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & b in C & 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: ( ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & a in C & b in C ) & ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & b in C & 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: ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & a in C & b in C ) and

A2: ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & b in C & 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 )

( C is_a_component_of (L~ f) ` & a in C & b in C ) & ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & b in C & 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: ( ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & a in C & b in C ) & ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & b in C & 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: ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & a in C & b in C ) and

A2: ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & b in C & 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 )

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

end;

suppose A3:
( a in RightComp 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 )

( C is_a_component_of (L~ f) ` & a in C & c in C ) ; :: thesis: verum

end;

( C is_a_component_of (L~ f) ` & a in C & c in C )

now :: thesis: ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & a in C & c in C )end;

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

per cases
( ( b in RightComp f & c in RightComp f ) or ( b in LeftComp f & c in LeftComp f ) )
by A2, Th14;

end;

suppose A4:
( b in RightComp 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 )

( C is_a_component_of (L~ f) ` & a in C & c in C )

RightComp f is_a_component_of (L~ f) `
by GOBOARD9:def 2;

hence ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & a in C & c in C ) by A3, A4; :: thesis: verum

end;hence ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & a in C & c in C ) by A3, A4; :: thesis: verum

suppose
( b in LeftComp 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 )

( C is_a_component_of (L~ f) ` & a in C & c in C )

then
LeftComp f meets RightComp f
by A3, 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:14; :: thesis: verum

end;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:14; :: thesis: verum

( C is_a_component_of (L~ f) ` & a in C & c in C ) ; :: thesis: verum

suppose A5:
( a in LeftComp 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 )

( C is_a_component_of (L~ f) ` & a in C & c in C ) ; :: thesis: verum

end;

( C is_a_component_of (L~ f) ` & a in C & c in C )

now :: thesis: ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & a in C & c in C )end;

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

per cases
( ( b in LeftComp f & c in LeftComp f ) or ( b in RightComp f & c in RightComp f ) )
by A2, Th14;

end;

suppose A6:
( b in LeftComp 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 )

( C is_a_component_of (L~ f) ` & a in C & c in C )

LeftComp f is_a_component_of (L~ f) `
by GOBOARD9:def 1;

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, A6; :: thesis: verum

end;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, A6; :: thesis: verum

suppose
( b in RightComp 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 )

( C is_a_component_of (L~ f) ` & a in C & c in C )

then
LeftComp f meets RightComp f
by A5, 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:14; :: thesis: verum

end;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:14; :: thesis: verum

( C is_a_component_of (L~ f) ` & a in C & c in C ) ; :: thesis: verum