let C be Simple_closed_curve; :: thesis: for n, m being Nat st n is_sufficiently_large_for C & n <= m holds
RightComp (Span (C,n)) c= RightComp (Span (C,m))
let n, m be Nat; :: thesis: ( n is_sufficiently_large_for C & n <= m implies RightComp (Span (C,n)) c= RightComp (Span (C,m)) )
assume that
A1: n is_sufficiently_large_for C and
A2: n <= m ; :: thesis: RightComp (Span (C,n)) c= RightComp (Span (C,m))
A3: L~ (Span (C,n)) misses RightComp (Span (C,n)) by SPRECT_3:25;
A4: RightComp (Span (C,n)) misses LeftComp (Span (C,n)) by GOBRD14:14;
Cl (LeftComp (Span (C,n))) = (LeftComp (Span (C,n))) \/ (L~ (Span (C,n))) by GOBRD14:22;
then Cl (LeftComp (Span (C,n))) misses RightComp (Span (C,n)) by A3, A4, XBOOLE_1:70;
then L~ (Span (C,m)) misses RightComp (Span (C,n)) by A1, A2, Th34, XBOOLE_1:63;
then A5: RightComp (Span (C,n)) c= (L~ (Span (C,m))) ` by SUBSET_1:23;
A6: RightComp (Span (C,m)) is_a_component_of (L~ (Span (C,m))) ` by GOBOARD9:def 2;
RightComp (Span (C,n)) meets RightComp (Span (C,m)) by A1, A2, Th32;
hence RightComp (Span (C,n)) c= RightComp (Span (C,m)) by A6, A5, GOBOARD9:4; :: thesis: verum