let C be Simple_closed_curve; :: thesis: for n, m being Element of NAT st n is_sufficiently_large_for C & n <= m holds
RightComp (Span C,n) c= RightComp (Span C,m)
let n, m be Element of 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: RightComp (Span C,n) meets RightComp (Span C,m) by A1, A2, Th33;
A4: RightComp (Span C,m) is_a_component_of (L~ (Span C,m)) ` by GOBOARD9:def 2;
A5: Cl (LeftComp (Span C,n)) = (LeftComp (Span C,n)) \/ (L~ (Span C,n)) by GOBRD14:32;
A6: L~ (Span C,n) misses RightComp (Span C,n) by SPRECT_3:42;
RightComp (Span C,n) misses LeftComp (Span C,n) by GOBRD14:24;
then Cl (LeftComp (Span C,n)) misses RightComp (Span C,n) by A5, A6, XBOOLE_1:70;
then L~ (Span C,m) misses RightComp (Span C,n) by A1, A2, Th35, XBOOLE_1:63;
then RightComp (Span C,n) c= (L~ (Span C,m)) ` by SUBSET_1:43;
hence RightComp (Span C,n) c= RightComp (Span C,m) by A3, A4, GOBOARD9:6; :: thesis: verum