assume A1: a in (LSeg ((NW-corner C),(NE-corner C))) /\ (LSeg ((NE-corner C),(SE-corner C))) ; :: thesis: a = NE-corner C
then a in LSeg ((NE-corner C),(SE-corner C)) by XBOOLE_0:def 4;
then a in { p where p is Point of (TOP-REAL 2) : ( p `1 = E-bound C & p `2 <= N-bound C & p `2 >= S-bound C ) } by Th23;
then A2: ex p being Point of (TOP-REAL 2) st
( p = a & p `1 = E-bound C & p `2 <= N-bound C & p `2 >= S-bound C ) ;
a in LSeg ((NW-corner C),(NE-corner C)) by A1, XBOOLE_0:def 4;
then a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = N-bound C ) } by Th25;
then ex p being Point of (TOP-REAL 2) st
( p = a & p `1 <= E-bound C & p `1 >= W-bound C & p `2 = N-bound C ) ;
hence a = NE-corner C by A2, EUCLID:53; :: thesis: verum