let p be Point of (TOP-REAL 2); :: thesis: ( p in west_halfline p & p in east_halfline p & p in north_halfline p & p in south_halfline p )
A1: p `2 = p `2 ;
p `1 <= p `1 ;
hence ( p in west_halfline p & p in east_halfline p & p in north_halfline p & p in south_halfline p ) by A1, Def10, Def11, Def12, Def13; :: thesis: verum