let C be Simple_closed_curve; 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; ( 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
; 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; verum