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 )
( p `1 <= p `1 & p `2 = p `2 ) ;
hence ( p in west_halfline p & p in east_halfline p & p in north_halfline p & p in south_halfline p ) by Def12, Def13, Def14, Def15; :: thesis: verum