let F be preordered Field; :: thesis: for P being Preordering of F
for a being non zero Element of F holds
( a in P \/ (- P) iff a " in P \/ (- P) )
let P be Preordering of F; :: thesis: for a being non zero Element of F holds
( a in P \/ (- P) iff a " in P \/ (- P) )
let a be non zero Element of F; :: thesis: ( a in P \/ (- P) iff a " in P \/ (- P) )
- a <> - (0. F) ;
then X: ( not a " is zero & not - (a ") is zero & not - a is zero ) by VECTSP_1:25;
hereby :: thesis: ( a " in P \/ (- P) implies a in P \/ (- P) )
assume a in P \/ (- P) ; :: thesis: a " in P \/ (- P)
per cases then ( a in P or a in - P ) by XBOOLE_0:def 3;
suppose a in - P ; :: thesis: a " in P \/ (- P)
then - a in - (- P) ;
then (- a) " in P by X, REALALG1:27;
then - ((- a) ") in - P ;
then a " in - P by YZ;
hence a " in P \/ (- P) by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
assume a " in P \/ (- P) ; :: thesis: a in P \/ (- P)
per cases then ( a " in P or a " in - P ) by XBOOLE_0:def 3;
suppose a " in P ; :: thesis: a in P \/ (- P)
then (a ") " in P by X, REALALG1:27;
hence a in P \/ (- P) by XBOOLE_0:def 3; :: thesis: verum
end;
suppose a " in - P ; :: thesis: a in P \/ (- P)
then - (a ") in - (- P) ;
then (- (a ")) " in P by X, REALALG1:27;
then - a in P by YY;
then - (- a) in - P ;
hence a in P \/ (- P) by XBOOLE_0:def 3; :: thesis: verum
end;
end;