let P be Subset of (TOP-REAL 2); :: thesis: for a being Point of (TOP-REAL 2) st a in BDD P holds

not south_halfline a c= UBD P

let a be Point of (TOP-REAL 2); :: thesis: ( a in BDD P implies not south_halfline a c= UBD P )

A1: ( BDD P misses UBD P & a in south_halfline a ) by JORDAN2C:24, TOPREAL1:38;

assume a in BDD P ; :: thesis: not south_halfline a c= UBD P

hence not south_halfline a c= UBD P by A1, XBOOLE_0:3; :: thesis: verum

not south_halfline a c= UBD P

let a be Point of (TOP-REAL 2); :: thesis: ( a in BDD P implies not south_halfline a c= UBD P )

A1: ( BDD P misses UBD P & a in south_halfline a ) by JORDAN2C:24, TOPREAL1:38;

assume a in BDD P ; :: thesis: not south_halfline a c= UBD P

hence not south_halfline a c= UBD P by A1, XBOOLE_0:3; :: thesis: verum