let C be being_simple_closed_curve Subset of (TOP-REAL 2); for D being Simple_closed_curve holds
( not C c= BDD D or not D c= BDD C )
let D be Simple_closed_curve; ( not C c= BDD D or not D c= BDD C )
assume that
A1:
C c= BDD D
and
A2:
D c= BDD C
; 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; verum