assume F_Complex is preordered ; :: thesis: contradiction
then reconsider F = F_Complex as preordered Field ;
consider P being Subset of F such that
A1: P is prepositive_cone by defpord;
reconsider P = P as Preordering of F by A1;
reconsider i = <i> as Element of F by COMPLFLD:def 1;
A2: QS F c= P by ord2;
- (1. F) = - 1r by COMPLFLD:2, COMPLFLD:8
.= <i> * <i>
.= i ^2 by COMPLFLD:4 ;
then - (1. F) is square ;
then - (1. F) in QS F ;
hence contradiction by A2, ord4; :: thesis: verum