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 )
A1: ( BDD P misses UBD P & a in east_halfline a ) by JORDAN2C:24, TOPREAL1:38;
assume a in BDD P ; :: thesis: not east_halfline a c= UBD P
hence not east_halfline a c= UBD P by A1, XBOOLE_0:3; :: thesis: verum