let C be Simple_closed_curve; :: thesis: for n, m being Element of NAT st n is_sufficiently_large_for C & n <= m holds
LeftComp (Span (C,m)) c= LeftComp (Span (C,n))
let n, m be Element of NAT ; :: thesis: ( n is_sufficiently_large_for C & n <= m implies LeftComp (Span (C,m)) c= LeftComp (Span (C,n)) )
assume that
A1: n is_sufficiently_large_for C and
A2: n <= m ; :: thesis: LeftComp (Span (C,m)) c= LeftComp (Span (C,n))
A3: (Cl (RightComp (Span (C,n)))) ` = LeftComp (Span (C,n)) by JORDAN1H:43;
A4: (Cl (RightComp (Span (C,m)))) ` = LeftComp (Span (C,m)) by JORDAN1H:43;
Cl (RightComp (Span (C,n))) c= Cl (RightComp (Span (C,m))) by A1, A2, Th36, PRE_TOPC:19;
hence LeftComp (Span (C,m)) c= LeftComp (Span (C,n)) by A3, A4, SUBSET_1:12; :: thesis: verum