let p be Point of (TOP-REAL 2); :: thesis: ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) )
A1: ( - (p `1) < p `2 implies - (- (p `1)) > - (p `2) ) by XREAL_1:24;
A2: ( - (p `1) > p `2 implies - (- (p `1)) < - (p `2) ) by XREAL_1:24;
assume ( not ( p `2 <= p `1 & - (p `1) <= p `2 ) & not ( p `2 >= p `1 & p `2 <= - (p `1) ) ) ; :: thesis: ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) )
hence ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) by A1, A2; :: thesis: verum