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)) c= Cl (RightComp (Span C,m)) by A1, A2, Th36, PRE_TOPC:49;
( (Cl (RightComp (Span C,n))) ` = LeftComp (Span C,n) & (Cl (RightComp (Span C,m))) ` = LeftComp (Span C,m) ) by JORDAN1H:51;
hence LeftComp (Span C,m) c= LeftComp (Span C,n) by A3, SUBSET_1:31; :: thesis: verum