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 )
per cases ( ( a in RightComp f & b in RightComp f ) or ( a in LeftComp f & b in LeftComp f ) ) by A1, Th14;
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 )
now :: 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 ( ( b in RightComp f & c in RightComp f ) or ( b in LeftComp f & c in LeftComp f ) ) by A2, Th14;
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 )
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;
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 )
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;
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 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 )
now :: 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 ( ( b in LeftComp f & c in LeftComp f ) or ( b in RightComp f & c in RightComp f ) ) by A2, Th14;
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 )
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;
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 )
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;
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;