let P be Subset of (TOP-REAL 2); :: thesis: for a being Point of (TOP-REAL 2) st a in BDD P holds
not east_halfline a c= UBD P
let a be Point of (TOP-REAL 2); :: thesis: ( a in BDD P implies not east_halfline a c= UBD P )
assume A1: a in BDD P ; :: thesis: not east_halfline a c= UBD P
A2: BDD P misses UBD P by JORDAN2C:28;
a in east_halfline a by TOPREAL1:45;
hence not east_halfline a c= UBD P by A1, A2, XBOOLE_0:3; :: thesis: verum