let C be Simple_closed_curve; :: thesis: for n being Nat st n is_sufficiently_large_for C holds
RightComp (Span (C,n)) c= BDD C
let n be Nat; :: thesis: ( n is_sufficiently_large_for C implies RightComp (Span (C,n)) c= BDD C )
assume n is_sufficiently_large_for C ; :: thesis: RightComp (Span (C,n)) c= BDD C
then BDD (L~ (Span (C,n))) c= BDD C by Th13;
hence RightComp (Span (C,n)) c= BDD C by GOBRD14:37; :: thesis: verum