let C be being_simple_closed_curve Subset of (TOP-REAL 2); :: thesis: for D being Simple_closed_curve st C c= BDD D holds
D c= UBD C
let D be Simple_closed_curve; :: thesis: ( C c= BDD D implies D c= UBD C )
assume A1: C c= BDD D ; :: thesis: D c= UBD C
assume A2: not D c= UBD C ; :: thesis: contradiction
C misses D by A1, JORDAN1A:7, XBOOLE_1:63;
then D c= BDD C by A2, JORDAN1K:19;
hence contradiction by A1, Th15; :: thesis: verum