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:26;
A2: ( - (p `1 ) > p `2 implies - (- (p `1 )) < - (p `2 ) ) by XREAL_1:26;
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