let a, b be set ; :: thesis: for f being non constant standard special_circular_sequence holds
( ( 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 ) ) ) iff ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) ) )
let f be non constant standard special_circular_sequence; :: thesis: ( ( 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 ) ) ) iff ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) ) )
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: ( ( ( 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 ) ) ) )

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: ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) )
A6: a in (LeftComp f) \/ (RightComp f) by A3, GOBRD12:10;
A7: b in (LeftComp f) \/ (RightComp f) by A4, GOBRD12:10;

per cases ( a in LeftComp f or a in RightComp f ) by A6, XBOOLE_0:def 3;

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

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

per cases ( b in LeftComp f or b in RightComp f ) by A7, XBOOLE_0:def 3;

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

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

end;

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

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

end;

end;

end;

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

end;

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

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

per cases ( b in RightComp f or b in LeftComp f ) by A7, XBOOLE_0:def 3;

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

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

end;

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

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

end;

end;

end;

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

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: verum

proof

assume A10: ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) ) ; :: thesis: ( 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 ) ) )
thus ( a in (L~ f) ` & b in (L~ f) ` ) :: thesis: 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 )

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 ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) ) by A10;

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

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

end;

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

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

end;

end;

end;

now :: thesis: 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 )

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: contradiction

now :: thesis: contradiction

per cases ( ( a in LeftComp f & b in RightComp f ) or ( a in RightComp f & b in LeftComp f ) ) by A10;

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

now :: thesis: contradiction

per cases ( C = LeftComp f or C misses LeftComp f ) by A1, A13, GOBOARD9:1;

suppose C = LeftComp f ; :: thesis: contradiction

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

end;

suppose C misses LeftComp f ; :: thesis: contradiction

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

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

now :: thesis: contradiction

per cases ( C = LeftComp f or C misses LeftComp f ) by A1, A13, GOBOARD9:1;

suppose C = LeftComp f ; :: thesis: contradiction

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

end;

suppose C misses LeftComp f ; :: thesis: contradiction

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

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

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: verum

end;