let C be being_simple_closed_curve Subset of (TOP-REAL 2); :: thesis: for D being Simple_closed_curve holds
( not C c= BDD D or not D c= BDD C )
let D be Simple_closed_curve; :: thesis: ( not C c= BDD D or not D c= BDD C )
assume that
A1: C c= BDD D and
A2: D c= BDD C ; :: thesis: contradiction
UBD C meets UBD D by Th12;
then consider e being object such that
A3: e in UBD C and
A4: e in UBD D by XBOOLE_0:3;
reconsider p = e as Point of (TOP-REAL 2) by A3;
UBD D misses BDD D by JORDAN2C:24;
then A5: not p in BDD D by A4, XBOOLE_0:3;
UBD C misses BDD C by JORDAN2C:24;
then A6: not p in BDD C by A3, XBOOLE_0:3;
then dist (p,C) <= dist (p,(BDD C)) by Th14;
then dist (p,(BDD D)) < dist (p,(BDD C)) by A1, A5, JORDAN1K:51, XXREAL_0:2;
then dist (p,(BDD D)) < dist (p,D) by A2, A6, JORDAN1K:51, XXREAL_0:2;
hence contradiction by A5, Th14; :: thesis: verum