realalg2.miz



    begin

    registration

      let X,Y be non empty set;

      cluster non emptyX -definedY -valued for Function;

      existence

      proof

        take (X --> the Element of Y);

        thus thesis;

      end;

    end

    registration

      cluster the carrier of F_Rat -> rational-membered;

      coherence by GAUSSINT:def 14;

    end

    theorem :: REALALG2:1

    

     P0: for L be right_zeroed non empty addLoopStr, S,T be Subset of L st ( 0. L) in T holds S c= (S + T)

    proof

      let L be right_zeroed non empty addLoopStr, S,T be Subset of L;

      assume

       A: ( 0. L) in T;

      let x be object;

      assume

       B: x in S;

      then

      reconsider a = x as Element of L;

      (a + ( 0. L)) in { (c + b) where c,b be Element of L : c in S & b in T } by A, B;

      hence x in (S + T) by RLVECT_1:def 4;

    end;

    theorem :: REALALG2:2

    for L be right_unital non empty multLoopStr, S,T be Subset of L st ( 1. L) in T holds S c= (S * T)

    proof

      let L be right_unital non empty multLoopStr, S,T be Subset of L;

      assume

       A: ( 1. L) in T;

      now

        let x be object;

        assume

         B: x in S;

        then

        reconsider a = x as Element of L;

        (a * ( 1. L)) in { (s1 * s2) where s1,s2 be Element of L : s1 in S & s2 in T } by A, B;

        hence x in (S * T);

      end;

      hence thesis;

    end;

    theorem :: REALALG2:3

    

     P1: for L be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr, S be Subset of L st ( 0. L) in S holds for a be Element of L holds S c= (S + (a * S))

    proof

      let L be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr, S be Subset of L;

      assume

       A: ( 0. L) in S;

      let a be Element of L;

      (a * ( 0. L)) in { (a * i) where i be Element of L : i in S } by A;

      hence thesis by P0;

    end;

    theorem :: REALALG2:4

    

     P2: for L be add-associative right_zeroed right_complementable right_unital right-distributive non empty doubleLoopStr, S be Subset of L st ( 0. L) in S & ( 1. L) in S holds for a be Element of L holds a in (S + (a * S))

    proof

      let L be add-associative right_zeroed right_complementable right_unital right-distributive non empty doubleLoopStr, S be Subset of L;

      assume

       AS: ( 0. L) in S & ( 1. L) in S;

      let a be Element of L;

      (a * ( 1. L)) in { (a * i) where i be Element of L : i in S } by AS;

      then (( 0. L) + (a * ( 1. L))) in { (c + b) where c,b be Element of L : c in S & b in (a * S) } by AS;

      hence thesis;

    end;

    theorem :: REALALG2:5

    

     c1: for R be add-associative right_zeroed right_complementable Abelian left-distributive non empty doubleLoopStr, a,b be Element of R, i be Integer holds (i '*' (a * b)) = ((i '*' a) * b)

    proof

      let R be add-associative right_zeroed right_complementable Abelian left-distributive non empty doubleLoopStr, a,b be Element of R, i be Integer;

      defpred P[ Integer] means ($1 '*' (a * b)) = (($1 '*' a) * b);

      

       A2: P[ 0 ]

      proof

        ( 0 '*' a) = ( 0. R) by RING_3: 59;

        hence ( 0 '*' (a * b)) = (( 0 '*' a) * b) by RING_3: 59;

      end;

      

       A3: for u be Integer holds P[u] implies P[(u - 1)] & P[(u + 1)]

      proof

        let u be Integer;

        assume

         A4: P[u];

        thus P[(u - 1)]

        proof

          set k = (u - 1);

          

           A6: ((k + 1) '*' (a * b)) = (((k '*' a) + (1 '*' a)) * b) by A4, RING_3: 62

          .= (((k '*' a) * b) + ((1 '*' a) * b)) by VECTSP_1:def 3

          .= (((k '*' a) * b) + (a * b)) by RING_3: 60;

          (((k '*' a) * b) + ( 0. R)) = (((k '*' a) * b) + ((a * b) + ( - (a * b)))) by RLVECT_1: 5

          .= (((k + 1) '*' (a * b)) + ( - (a * b))) by A6, RLVECT_1:def 3;

          

          hence ((k '*' a) * b) = (((k + 1) '*' (a * b)) + (( - 1) '*' (a * b))) by RING_3: 61

          .= (k '*' (a * b)) by RING_3: 62;

        end;

        thus P[(u + 1)]

        proof

          set k = (u + 1);

          

           A6: ((k - 1) '*' (a * b)) = (((k '*' a) - (1 '*' a)) * b) by A4, RING_3: 64

          .= (((k '*' a) * b) + (( - (1 '*' a)) * b)) by VECTSP_1:def 3

          .= (((k '*' a) * b) + ( - ((1 '*' a) * b))) by VECTSP_1: 9

          .= (((k '*' a) * b) - (a * b)) by RING_3: 60;

          (((k '*' a) * b) + ( 0. R)) = (((k '*' a) * b) + (( - (a * b)) + (a * b))) by RLVECT_1: 5

          .= (((k - 1) '*' (a * b)) + (a * b)) by A6, RLVECT_1:def 3;

          

          hence ((k '*' a) * b) = (((k - 1) '*' (a * b)) + (1 '*' (a * b))) by RING_3: 60

          .= (k '*' (a * b)) by RING_3: 62;

        end;

      end;

      for i be Integer holds P[i] from INT_1:sch 4( A2, A3);

      hence thesis;

    end;

    theorem :: REALALG2:6

    

     c1a: for R be add-associative right_zeroed right_complementable Abelian left-distributive non empty doubleLoopStr, a be Element of R, i be Integer holds (i '*' ( - a)) = ( - (i '*' a))

    proof

      let R be add-associative right_zeroed right_complementable Abelian left-distributive non empty doubleLoopStr, a be Element of R, i be Integer;

      defpred P[ Integer] means ($1 '*' ( - a)) = ( - ($1 '*' a));

      

       A2: P[ 0 ]

      proof

        ( 0 '*' ( - a)) = ( - ( 0. R)) by RING_3: 59

        .= ( - ( 0 '*' a)) by RING_3: 59;

        hence ( 0 '*' ( - a)) = ( - ( 0 '*' a));

      end;

      

       A3: for u be Integer holds P[u] implies P[(u - 1)] & P[(u + 1)]

      proof

        let u be Integer;

        assume

         A4: P[u];

        thus P[(u - 1)]

        proof

          set k = (u - 1);

          

           A6: ((k + 1) '*' ( - a)) = ( - ((k '*' a) + (1 '*' a))) by A4, RING_3: 62

          .= ( - ((k '*' a) + a)) by RING_3: 60

          .= (( - (k '*' a)) + ( - a)) by RLVECT_1: 31;

          

          thus ( - (k '*' a)) = (( - (k '*' a)) + ( 0. R))

          .= (( - (k '*' a)) + (( - a) + a)) by RLVECT_1: 5

          .= (((k + 1) '*' ( - a)) + a) by A6, RLVECT_1:def 3

          .= (((k '*' ( - a)) + (1 '*' ( - a))) + a) by RING_3: 62

          .= (((k '*' ( - a)) + ( - a)) + a) by RING_3: 60

          .= ((k '*' ( - a)) + (( - a) + a)) by RLVECT_1:def 3

          .= ((k '*' ( - a)) + ( 0. R)) by RLVECT_1: 5

          .= (k '*' ( - a));

        end;

        thus P[(u + 1)]

        proof

          set k = (u + 1);

          

           A6: ((k - 1) '*' ( - a)) = ( - ((k '*' a) - (1 '*' a))) by A4, RING_3: 64

          .= ( - ((k '*' a) - a)) by RING_3: 60

          .= (( - (k '*' a)) + ( - ( - a))) by RLVECT_1: 33;

          

          thus ( - (k '*' a)) = (( - (k '*' a)) + ( 0. R))

          .= (( - (k '*' a)) + (a + ( - a))) by RLVECT_1: 5

          .= (((k - 1) '*' ( - a)) + ( - a)) by A6, RLVECT_1:def 3

          .= (((k '*' ( - a)) - (1 '*' ( - a))) + ( - a)) by RING_3: 64

          .= (((k '*' ( - a)) - ( - a)) + ( - a)) by RING_3: 60

          .= ((k '*' ( - a)) + (( - a) + a)) by RLVECT_1:def 3

          .= ((k '*' ( - a)) + ( 0. R)) by RLVECT_1: 5

          .= (k '*' ( - a));

        end;

      end;

      for i be Integer holds P[i] from INT_1:sch 4( A2, A3);

      hence thesis;

    end;

    registration

      let R be Ring;

      let a be Element of R;

      cluster (a ^2 ) -> square;

      coherence ;

      cluster (a |^ 2) -> square;

      coherence

      proof

        (a |^ 2) = (a ^2 ) by RING_5: 3;

        hence thesis;

      end;

    end

    theorem :: REALALG2:7

    

     P3: for R be commutative Ring, a,b be Element of R holds ((a + b) ^2 ) = (((a ^2 ) + ((2 '*' a) * b)) + (b ^2 ))

    proof

      let R be commutative Ring;

      let a,b be Element of R;

      

      thus ((a + b) ^2 ) = ((a * (a + b)) + (b * (a + b))) by VECTSP_1:def 7

      .= (((a * a) + (a * b)) + (b * (a + b))) by VECTSP_1:def 7

      .= (((a * a) + (a * b)) + ((b * a) + (b * b))) by VECTSP_1:def 7

      .= ((a * a) + ((a * b) + ((b * a) + (b * b)))) by RLVECT_1:def 3

      .= ((a ^2 ) + (((a * b) + (b * a)) + (b * b))) by RLVECT_1:def 3

      .= ((a ^2 ) + ((2 '*' (a * b)) + (b ^2 ))) by RING_5: 2

      .= (((a ^2 ) + (2 '*' (a * b))) + (b ^2 )) by RLVECT_1:def 3

      .= (((a ^2 ) + ((2 '*' a) * b)) + (b ^2 )) by c1;

    end;

    theorem :: REALALG2:8

    

     P4: for R be commutative Ring, a,b be Element of R holds ((a - b) ^2 ) = (((a ^2 ) - ((2 '*' a) * b)) + (b ^2 ))

    proof

      let R be commutative Ring;

      let a,b be Element of R;

      

      thus ((a - b) ^2 ) = (((a ^2 ) + ((2 '*' a) * ( - b))) + (( - b) ^2 )) by P3

      .= (((a ^2 ) + (2 '*' (a * ( - b)))) + (( - b) ^2 )) by c1

      .= (((a ^2 ) + (2 '*' ( - (a * b)))) + (( - b) ^2 )) by VECTSP_1: 8

      .= (((a ^2 ) + ( - (2 '*' (a * b)))) + (( - b) ^2 )) by c1a

      .= (((a ^2 ) - ((2 '*' a) * b)) + (( - b) ^2 )) by c1

      .= (((a ^2 ) - ((2 '*' a) * b)) + (b ^2 )) by VECTSP_1: 10;

    end;

    theorem :: REALALG2:9

    

     P4a: for R be commutative Ring, a,b be Element of R holds ((a + b) * (a - b)) = ((a ^2 ) - (b ^2 ))

    proof

      let R be commutative Ring;

      let a,b be Element of R;

      

      thus ((a + b) * (a - b)) = ((a * (a - b)) + (b * (a - b))) by VECTSP_1:def 7

      .= (((a * a) + (a * ( - b))) + (b * (a + ( - b)))) by VECTSP_1:def 7

      .= (((a * a) + (a * ( - b))) + ((b * a) + (b * ( - b)))) by VECTSP_1:def 7

      .= ((a * a) + ((a * ( - b)) + ((b * a) + (b * ( - b))))) by RLVECT_1:def 3

      .= ((a * a) + (((a * ( - b)) + (b * a)) + (b * ( - b)))) by RLVECT_1:def 3

      .= ((a * a) + ((( - (a * b)) + (b * a)) + (b * ( - b)))) by VECTSP_1: 8

      .= ((a * a) + (( 0. R) + (b * ( - b)))) by RLVECT_1: 5

      .= ((a ^2 ) - (b ^2 )) by VECTSP_1: 8;

    end;

    

     P5b: for R be non degenerated Ring holds ( Char R) = 2 iff (2 '*' ( 1. R)) = ( 0. R)

    proof

      let R be non degenerated Ring;

      now

        assume

         AS: (2 '*' ( 1. R)) = ( 0. R);

        now

          let m be positive Nat;

          assume m < 2;

          then m < (1 + 1);

          then m <= 1 by NAT_1: 13;

          then m = 0 or ... or m = 1;

          hence (m '*' ( 1. R)) <> ( 0. R) by RING_3: 60;

        end;

        hence ( Char R) = 2 by AS, RING_3:def 5;

      end;

      hence thesis by RING_3:def 5;

    end;

    theorem :: REALALG2:10

    

     sq00: for R be domRing, a,b be Element of R holds (a ^2 ) = (b ^2 ) iff (a = b or a = ( - b))

    proof

      let R be domRing, a,b be Element of R;

      hereby

        assume (a ^2 ) = (b ^2 );

        

        then ( 0. R) = ((a ^2 ) - (b ^2 )) by RLVECT_1: 15

        .= ((a + b) * (a - b)) by P4a;

        per cases by VECTSP_2:def 1;

          suppose (a + b) = ( 0. R);

          hence a = b or a = ( - b) by RLVECT_1: 6;

        end;

          suppose (a - b) = ( 0. R);

          hence a = b or a = ( - b) by RLVECT_1: 21;

        end;

      end;

      assume a = b or a = ( - b);

      per cases ;

        suppose a = b;

        hence (a ^2 ) = (b ^2 );

      end;

        suppose a = ( - b);

        hence (a ^2 ) = (b ^2 ) by VECTSP_1: 10;

      end;

    end;

    theorem :: REALALG2:11

    

     XZ: for F be Field, a be non zero Element of F holds (( - a) " ) = ( - (a " ))

    proof

      let F be Field, a be non zero Element of F;

      

       X: (a " ) is non zero & ( - (a " )) is non zero by VECTSP_1: 25;

      (( - (a " )) * ( - a)) = ((a " ) * a) by VECTSP_1: 10

      .= ( 1_ F) by X, VECTSP_2: 9;

      hence (( - a) " ) = ( - (a " )) by VECTSP_2: 10;

    end;

    theorem :: REALALG2:12

    

     YY: for F be Field, a be non zero Element of F holds (( - (a " )) " ) = ( - a)

    proof

      let F be Field, a be non zero Element of F;

      

       X: (a " ) is non zero & ( - (a " )) is non zero by VECTSP_1: 25;

      (( - ((a " ) " )) * ( - (a " ))) = (((a " ) " ) * (a " )) by VECTSP_1: 10

      .= ( 1_ F) by X, VECTSP_2: 9;

      hence (( - (a " )) " ) = ( - a) by VECTSP_2: 10;

    end;

    theorem :: REALALG2:13

    

     YZ: for F be Field, a be non zero Element of F holds ( - (( - a) " )) = (a " )

    proof

      let F be Field, a be non zero Element of F;

      ((a " ) - ( - (( - a) " ))) = ((a " ) + ( - (a " ))) by XZ

      .= ( 0. F) by RLVECT_1: 5;

      hence thesis by RLVECT_1: 21;

    end;

    theorem :: REALALG2:14

    

     P5a: for F be Field, a be Element of F, b be non zero Element of F holds ((a / b) ^2 ) = ((a ^2 ) / (b ^2 ))

    proof

      let F be Field;

      let a be Element of F, b be non zero Element of F;

      

       H1: b <> ( 0. F);

      

      thus ((a / b) ^2 ) = (a * ((b " ) * (a * (b " )))) by GROUP_1:def 3

      .= (a * (a * ((b " ) * (b " )))) by GROUP_1:def 3

      .= ((a * a) * ((b " ) * (b " ))) by GROUP_1:def 3

      .= ((a ^2 ) / (b ^2 )) by VECTSP_2: 11, H1;

    end;

    theorem :: REALALG2:15

    

     P5: for F be Field st ( Char F) <> 2 holds for a be Element of F holds ((((a + ( 1. F)) / (2 '*' ( 1. F))) ^2 ) - (((a - ( 1. F)) / (2 '*' ( 1. F))) ^2 )) = a

    proof

      let F be Field;

      assume

       AS: ( Char F) <> 2;

      let a be Element of F;

      (2 '*' ( 1. F)) <> ( 0. F) by AS, P5b;

      then

       A1: ((2 '*' ( 1. F)) * (2 '*' ( 1. F))) <> ( 0. F) by VECTSP_1: 12;

      then

       C: ((2 * 2) '*' ( 1. F)) <> ( 0. F) by RING_3: 67;

      

       D: (2 '*' ( 1. F)) is non zero by AS, P5b;

      

      thus ((((a + ( 1. F)) / (2 '*' ( 1. F))) ^2 ) - (((a - ( 1. F)) / (2 '*' ( 1. F))) ^2 )) = ((((a + ( 1. F)) ^2 ) / ((2 '*' ( 1. F)) ^2 )) - (((a - ( 1. F)) / (2 '*' ( 1. F))) ^2 )) by D, P5a

      .= ((((a + ( 1. F)) ^2 ) / ((2 '*' ( 1. F)) ^2 )) - (((a - ( 1. F)) ^2 ) / ((2 '*' ( 1. F)) ^2 ))) by D, P5a

      .= ((((a + ( 1. F)) ^2 ) - ((a - ( 1. F)) ^2 )) / ((2 '*' ( 1. F)) ^2 )) by A1, VECTSP_2: 20

      .= (((((a ^2 ) + ((2 '*' a) * ( 1. F))) + (( 1. F) ^2 )) - ((a - ( 1. F)) ^2 )) / ((2 '*' ( 1. F)) ^2 )) by P3

      .= (((((a ^2 ) + (2 '*' a)) + (( 1. F) ^2 )) - (((a ^2 ) - ((2 '*' a) * ( 1. F))) + (( 1. F) ^2 ))) / ((2 '*' ( 1. F)) ^2 )) by P4

      .= (((((a ^2 ) + (2 '*' a)) + (( 1. F) ^2 )) + (( - ((a ^2 ) + ( - (2 '*' a)))) + ( - (( 1. F) ^2 )))) / ((2 '*' ( 1. F)) ^2 )) by RLVECT_1: 31

      .= (((((a ^2 ) + (2 '*' a)) + (( 1. F) ^2 )) + ((( - (a ^2 )) + ( - ( - (2 '*' a)))) + ( - (( 1. F) ^2 )))) / ((2 '*' ( 1. F)) ^2 )) by RLVECT_1: 31

      .= ((((a ^2 ) + (2 '*' a)) + ((( 1. F) ^2 ) + (( - (( 1. F) ^2 )) + (( - (a ^2 )) + (2 '*' a))))) / ((2 '*' ( 1. F)) ^2 )) by RLVECT_1:def 3

      .= ((((a ^2 ) + (2 '*' a)) + (((( 1. F) ^2 ) + ( - (( 1. F) ^2 ))) + (( - (a ^2 )) + (2 '*' a)))) / ((2 '*' ( 1. F)) ^2 )) by RLVECT_1:def 3

      .= ((((a ^2 ) + (2 '*' a)) + (( 0. F) + (( - (a ^2 )) + (2 '*' a)))) / ((2 '*' ( 1. F)) ^2 )) by RLVECT_1: 5

      .= (((2 '*' a) + ((a ^2 ) + (( - (a ^2 )) + (2 '*' a)))) / ((2 '*' ( 1. F)) ^2 )) by RLVECT_1:def 3

      .= (((2 '*' a) + (((a ^2 ) + ( - (a ^2 ))) + (2 '*' a))) / ((2 '*' ( 1. F)) ^2 )) by RLVECT_1:def 3

      .= (((2 '*' a) + (( 0. F) + (2 '*' a))) / ((2 '*' ( 1. F)) ^2 )) by RLVECT_1: 5

      .= (((2 + 2) '*' a) / ((2 '*' ( 1. F)) ^2 )) by RING_3: 62

      .= ((4 '*' a) / ((2 * 2) '*' ( 1. F))) by RING_3: 67

      .= ((4 '*' (( 1. F) * a)) / (4 '*' ( 1. F)))

      .= (((4 '*' ( 1. F)) * a) / (4 '*' ( 1. F))) by c1

      .= (a / ((4 '*' ( 1. F)) / (4 '*' ( 1. F)))) by C, VECTSP_2: 21

      .= (a / ( 1_ F)) by C, VECTSP_2: 17

      .= a;

    end;

    registration

      cluster preordered -> 0 -characteristic for non degenerated Ring;

      coherence by REALALG1: 28;

    end

    theorem :: REALALG2:16

    

     v1a: for R be preordered Ring, P be Preordering of R holds (( - P) * P) = (P * ( - P))

    proof

      let R be preordered Ring, P be Preordering of R;

       A:

      now

        let o be object;

        assume o in (( - P) * P);

        then

        consider a,b be Element of R such that

         A1: o = (a * b) & a in ( - P) & b in P;

        consider c be Element of R such that

         A2: a = ( - c) & c in P by A1;

        

         A3: ( - b) in ( - P) by A1;

        (c * ( - b)) = ( - (c * b)) by VECTSP_1: 8

        .= (a * b) by A2, VECTSP_1: 9;

        hence o in (P * ( - P)) by A1, A2, A3;

      end;

      now

        let o be object;

        assume o in (P * ( - P));

        then

        consider a,b be Element of R such that

         A1: o = (a * b) & a in P & b in ( - P);

        consider c be Element of R such that

         A2: b = ( - c) & c in P by A1;

        

         A3: ( - a) in ( - P) by A1;

        (( - a) * c) = ( - (a * c)) by VECTSP_1: 9

        .= (a * b) by A2, VECTSP_1: 8;

        hence o in (( - P) * P) by A1, A2, A3;

      end;

      hence thesis by A, TARSKI: 2;

    end;

    theorem :: REALALG2:17

    

     v1: for R be preordered Ring, P be Preordering of R holds (( - P) + ( - P)) c= ( - P) & (( - P) * ( - P)) c= P

    proof

      let R be preordered Ring, P be Preordering of R;

      

       X: (P + P) c= P & (P * P) c= P by REALALG1:def 14;

      hereby

        let o be object;

        assume o in (( - P) + ( - P));

        then

        consider a,b be Element of R such that

         A: o = (a + b) & a in ( - P) & b in ( - P);

        ( - a) in ( - ( - P)) & ( - b) in ( - ( - P)) by A;

        then (( - a) + ( - b)) in (P + P);

        then (( - a) + ( - b)) in P by X;

        then ( - (a + b)) in P by RLVECT_1: 31;

        then ( - ( - (a + b))) in ( - P);

        hence o in ( - P) by A;

      end;

      let o be object;

      assume o in (( - P) * ( - P));

      then

      consider a,b be Element of R such that

       A: o = (a * b) & a in ( - P) & b in ( - P);

      ( - a) in ( - ( - P)) & ( - b) in ( - ( - P)) by A;

      then (( - a) * ( - b)) in (P * P);

      then (( - a) * ( - b)) in P by X;

      hence o in P by A, VECTSP_1: 10;

    end;

    theorem :: REALALG2:18

    

     v2: for R be preordered Ring, P be Preordering of R holds (( - P) * P) c= ( - P) & (P * ( - P)) c= ( - P)

    proof

      let R be preordered Ring, P be Preordering of R;

      hereby

        let o be object;

        assume o in (( - P) * P);

        then

        consider a,b be Element of R such that

         A: o = (a * b) & a in ( - P) & b in P;

        ( - b) in ( - P) by A;

        then

         B: (a * ( - b)) in (( - P) * ( - P)) by A;

        (( - P) * ( - P)) c= P by v1;

        then (a * ( - b)) in P by B;

        then ( - (a * b)) in P by VECTSP_1: 8;

        then ( - ( - (a * b))) in ( - P);

        hence o in ( - P) by A;

      end;

      then (( - P) * P) c= ( - P);

      hence thesis by v1a;

    end;

    theorem :: REALALG2:19

    

     spa: for R be preordered Ring, P be Preordering of R holds for n be Nat holds (n '*' ( 1. R)) in P

    proof

      let R be preordered Ring, P be Preordering of R;

      

       X: (P + P) c= P by REALALG1:def 14;

      defpred P[ Nat] means ($1 '*' ( 1. R)) in P;

      ( 0 '*' ( 1. R)) = ( 0. R) by RING_3: 59;

      then

       IA: P[ 0 ] by REALALG1: 25;

       IS:

      now

        let k be Nat;

        assume

         IV: P[k];

        

         A: ((k + 1) '*' ( 1. R)) = ((k '*' ( 1. R)) + (1 '*' ( 1. R))) by RING_3: 62

        .= ((k '*' ( 1. R)) + ( 1. R)) by RING_3: 60;

        ( 1. R) in P by REALALG1: 25;

        then ((k + 1) '*' ( 1. R)) in (P + P) by IV, A;

        hence P[(k + 1)] by X;

      end;

      

       I: for k be Nat holds P[k] from NAT_1:sch 2( IA, IS);

      thus thesis by I;

    end;

    

     Lm8: for i be Integer holds (i '*' ( 1. INT.Ring )) = i

    proof

      let i be Integer;

      set R = INT.Ring ;

      defpred P[ Integer] means $1 = ($1 '*' ( 1. R));

      ( 0 '*' ( 1. R)) = ( 0. R) by RING_3: 59;

      then

       A1: P[ 0 ];

       A2:

      now

        let u be Integer;

        assume

         A3: P[u];

        ((u - 1) '*' ( 1. R)) = ((u '*' ( 1. R)) - (1 '*' ( 1. R))) by RING_3: 64

        .= (u - 1) by A3, RING_3: 60;

        hence P[(u - 1)];

        ((u + 1) '*' ( 1. R)) = ((u '*' ( 1. R)) + (1 '*' ( 1. R))) by RING_3: 62

        .= (u + 1) by A3, RING_3: 60;

        hence P[(u + 1)];

      end;

      for k be Integer holds P[k] from INT_1:sch 4( A1, A2);

      hence (i '*' ( 1. INT.Ring )) = i;

    end;

    

     Lm9: for i be Integer holds (i '*' ( 1. F_Rat )) = i

    proof

      let i be Integer;

      set R = F_Rat ;

      defpred P[ Integer] means $1 = ($1 '*' ( 1. R));

      ( 0 '*' ( 1. R)) = ( 0. R) by RING_3: 59;

      then

       A1: P[ 0 ] by GAUSSINT:def 14;

       A2:

      now

        let u be Integer;

        assume

         A3: P[u];

        ((u - 1) '*' ( 1. R)) = ((u '*' ( 1. R)) - (1 '*' ( 1. R))) by RING_3: 64

        .= (u - 1) by A3, GAUSSINT:def 14, RING_3: 60;

        hence P[(u - 1)];

        ((u + 1) '*' ( 1. R)) = ((u '*' ( 1. R)) + (1 '*' ( 1. R))) by RING_3: 62

        .= (u + 1) by A3, GAUSSINT:def 14, RING_3: 60;

        hence P[(u + 1)];

      end;

      for k be Integer holds P[k] from INT_1:sch 4( A1, A2);

      hence (i '*' ( 1. R)) = i;

    end;

    registration

      cluster -> spanning for Preordering of INT.Ring ;

      coherence

      proof

        set R = INT.Ring ;

        let P be Preordering of INT.Ring ;

        now

          let o be object;

          assume o in the carrier of R;

          then

          consider n be Nat such that

           B: o = n or o = ( - n) by INT_1: 2;

          

           A: (n '*' ( 1. R)) = n by Lm8;

          

           C: ( - (n '*' ( 1. R))) = ( - n) by Lm8;

          per cases by B;

            suppose o = n;

            then o in P by A, spa;

            hence o in (P \/ ( - P)) by XBOOLE_0:def 3;

          end;

            suppose

             K: o = ( - n);

            n in P by A, spa;

            then ( - n) in ( - P) by C;

            hence o in (P \/ ( - P)) by K, XBOOLE_0:def 3;

          end;

        end;

        then the carrier of R = (P \/ ( - P)) by TARSKI:def 3;

        hence P is spanning;

      end;

      cluster -> spanning for Preordering of F_Rat ;

      coherence

      proof

        set R = F_Rat ;

        let P be Preordering of R;

        

         A: ( 0. F_Rat ) = 0 & ( 1. F_Rat ) = 1 by GAUSSINT:def 14;

        

         E: (P + P) c= P & (P * P) c= P by REALALG1:def 14;

        

         H: (( - P) * P) c= ( - P) by v2;

        now

          let o be object;

          assume o in the carrier of R;

          then

          reconsider p = o as Rational;

          set m = ( numerator p), n = ( denominator p);

          reconsider a = n, b = m as Element of F_Rat by INT_1:def 2, NUMBERS: 14, GAUSSINT:def 14;

          

           G: a <> ( 0. R) by GAUSSINT:def 14, RAT_1: 11;

          

           F: p = (m * (n " )) by RAT_1: 15

          .= (b * (a " )) by G, GAUSSINT: 15;

          per cases ;

            suppose m = 0 ;

            then p = 0 by RAT_1: 14;

            then o in P by A, REALALG1: 25;

            hence o in (P \/ ( - P)) by XBOOLE_0:def 3;

          end;

            suppose 0 < m;

            then

            reconsider m1 = m as Element of NAT by INT_1: 3;

            

             C: (n '*' ( 1. R)) = n & (m1 '*' ( 1. R)) = m1 by Lm9;

            then

             D: a in P & b in P by spa;

            a is non zero by GAUSSINT:def 14, RAT_1: 11;

            then (a " ) in P by C, spa, REALALG1: 27;

            then (b * (a " )) in (P * P) by D;

            hence o in (P \/ ( - P)) by E, F, XBOOLE_0:def 3;

          end;

            suppose m < 0 ;

            then

            reconsider m1 = ( - m) as Element of NAT by INT_1: 3;

            

             E: (n '*' ( 1. R)) = n & (m1 '*' ( 1. R)) = m1 by Lm9;

            then a in P & ( - b) in P by spa;

            then

             D: a in P & ( - ( - b)) in ( - P);

            a is non zero by GAUSSINT:def 14, RAT_1: 11;

            then (a " ) in P by E, spa, REALALG1: 27;

            then (b * (a " )) in (( - P) * P) by D;

            hence o in (P \/ ( - P)) by F, H, XBOOLE_0:def 3;

          end;

        end;

        then the carrier of R = (P \/ ( - P)) by TARSKI:def 3;

        hence P is spanning;

      end;

      cluster -> spanning for Preordering of F_Real ;

      coherence

      proof

        set R = F_Real ;

        let P be Preordering of R;

        

         A: ( SQ R) c= P by REALALG1:def 14;

        now

          let o be object;

          assume o in the carrier of R;

          then

          reconsider x = o as Element of REAL ;

          per cases ;

            suppose

             B: 0 <= x;

            reconsider r = ( sqrt x) as Element of REAL by XREAL_0:def 1;

            reconsider a = r as Element of F_Real ;

            x = (( sqrt x) ^2 ) by SQUARE_1:def 2, B

            .= (a * a)

            .= (a |^ 2) by RING_5: 3;

            then x in ( SQ R);

            hence o in (P \/ ( - P)) by A, XBOOLE_0:def 3;

          end;

            suppose

             B: x <= 0 ;

            reconsider r = ( sqrt ( - x)) as Element of REAL by XREAL_0:def 1;

            reconsider a = r as Element of F_Real ;

            

             C: ( - x) = (( sqrt ( - x)) ^2 ) by SQUARE_1:def 2, B

            .= (a * a)

            .= (a |^ 2) by RING_5: 3;

            then ( - x) in ( SQ R);

            then ( - (a |^ 2)) in ( - P) by A, C;

            hence o in (P \/ ( - P)) by C, XBOOLE_0:def 3;

          end;

        end;

        then the carrier of R = (P \/ ( - P)) by TARSKI:def 3;

        hence P is spanning;

      end;

    end

    theorem :: REALALG2:20

    for P be Preordering of INT.Ring holds P = Positives(INT.Ring) by REALALG1: 40;

    theorem :: REALALG2:21

    for P be Preordering of F_Rat holds P = Positives(F_Rat) by REALALG1: 38;

    theorem :: REALALG2:22

    for P be Preordering of F_Real holds P = Positives(F_Real) by REALALG1: 36;

    begin

    theorem :: REALALG2:23

    for R be Ring holds ( Char R) = 1 iff R is degenerated

    proof

      let R be Ring;

      hereby

        assume ( Char R) = 1;

        then (1 '*' ( 1. R)) = ( 0. R) & 1 <> 0 & for m be positive Nat st m < 1 holds (m '*' ( 1. R)) <> ( 0. R) by RING_3:def 5;

        hence R is degenerated by RING_3: 60;

      end;

      assume R is degenerated;

      then

       A: (1 '*' ( 1. R)) = ( 0. R) by RING_3: 60;

      for m be positive Nat st m < 1 holds (m '*' ( 1. R)) <> ( 0. R) by NAT_1: 14;

      hence ( Char R) = 1 by A, RING_3:def 5;

    end;

    theorem :: REALALG2:24

    for R be non degenerated Ring holds ( Char R) = 2 iff (2 '*' ( 1. R)) = ( 0. R) by P5b;

    theorem :: REALALG2:25

    

     char4: for R be domRing holds ( Char R) = 0 iff for a be non zero Element of R, n be non zero Nat holds (n '*' a) <> ( 0. R)

    proof

      let R be domRing;

      hereby

        assume

         AS: ( Char R) = 0 ;

        now

          given a be non zero Element of R, n be non zero Nat such that

           H: (n '*' a) = ( 0. R);

          ( 0. R) = (n '*' (( 1. R) * a)) by H

          .= ((n '*' ( 1. R)) * a) by c1;

          then (n '*' ( 1. R)) = ( 0. R) by VECTSP_2:def 1;

          hence contradiction by AS, RING_3:def 5;

        end;

        hence for a be non zero Element of R, n be non zero Nat holds (n '*' a) <> ( 0. R);

      end;

      assume

       AS: for a be non zero Element of R, n be non zero Nat holds (n '*' a) <> ( 0. R);

      now

        assume ( Char R) <> 0 ;

        then

         H1: ( CharSet R) <> {} by RING_3: 78;

        let x be Element of ( CharSet R);

        x in ( CharSet R) by H1;

        then ex n be positive Nat st x = n & (n '*' ( 1. R)) = ( 0. R);

        hence contradiction by AS;

      end;

      hence ( Char R) = 0 ;

    end;

    theorem :: REALALG2:26

    

     tA: for R be 0 -characteristic domRing, a be Element of R holds ( - a) = a iff a = ( 0. R)

    proof

      let R be 0 -characteristic domRing, a be Element of R;

      hereby

        assume ( - a) = a;

        then (a + a) = ( 0. R) by RLVECT_1: 5;

        

        then

         C: ( 0. R) = ((1 '*' a) + a) by RING_3: 60

        .= ((1 '*' a) + (1 '*' a)) by RING_3: 60

        .= ((1 + 1) '*' a) by RING_3: 62;

        ( Char R) = 0 by RING_3:def 6;

        then a is zero by C, char4;

        hence a = ( 0. R);

      end;

      thus thesis;

    end;

    begin

    definition

      let R be preordered Ring, P be Preordering of R;

      :: REALALG2:def1

      attr P is maximal means

      : defmax: for Q be Preordering of R st P c= Q holds P = Q;

    end

    theorem :: REALALG2:27

    

     T2: for F be preordered Field, P be Preordering of F, a be Element of F st not ( - a) in P holds (P + (a * P)) is Preordering of F

    proof

      let F be preordered Field, P be Preordering of F, a be Element of F;

      assume

       ASS: not ( - a) in P;

      

       X: ( 0. F) in P & ( 1. F) in P & (P + P) c= P & (P * P) c= P & (P /\ ( - P)) = {( 0. F)} & ( SQ F) c= P by REALALG1: 25, REALALG1:def 14;

      set S = (P + (a * P));

      

       A: (S + S) c= S

      proof

        let o be object;

        assume o in (S + S);

        then

        consider c,b be Element of F such that

         H1: o = (c + b) & c in S & b in S;

        consider c1,c2 be Element of F such that

         H2: c = (c1 + c2) & c1 in P & c2 in (a * P) by H1;

        consider b1,b2 be Element of F such that

         H3: b = (b1 + b2) & b1 in P & b2 in (a * P) by H1;

        consider c3 be Element of F such that

         H4: c2 = (a * c3) & c3 in P by H2;

        consider b3 be Element of F such that

         H5: b2 = (a * b3) & b3 in P by H3;

        

         H6: (c3 + b3) in (P + P) by H4, H5;

        (c2 + b2) = (a * (c3 + b3)) by H4, H5, VECTSP_1:def 3;

        then

         H7: (c2 + b2) in (a * P) by H6, X;

        

         H8: (c1 + b1) in (P + P) by H3, H2;

        ((c1 + b1) + (c2 + b2)) = (((c1 + b1) + c2) + b2) by RLVECT_1:def 3

        .= (((c1 + c2) + b1) + b2) by RLVECT_1:def 3

        .= o by H1, H2, H3, RLVECT_1:def 3;

        hence o in S by H8, H7, X;

      end;

      

       B: (S * S) c= S

      proof

        let o be object;

        assume o in (S * S);

        then

        consider c,b be Element of F such that

         H1: o = (c * b) & c in S & b in S;

        consider c1,c2 be Element of F such that

         H2: c = (c1 + c2) & c1 in P & c2 in (a * P) by H1;

        consider b1,b2 be Element of F such that

         H3: b = (b1 + b2) & b1 in P & b2 in (a * P) by H1;

        consider c3 be Element of F such that

         H4: c2 = (a * c3) & c3 in P by H2;

        consider b3 be Element of F such that

         H5: b2 = (a * b3) & b3 in P by H3;

        

         H6: o = ((c1 * (b1 + (a * b3))) + ((a * c3) * (b1 + (a * b3)))) by H1, H2, H3, H4, H5, VECTSP_1:def 3

        .= (((c1 * b1) + (c1 * (a * b3))) + ((a * c3) * (b1 + (a * b3)))) by VECTSP_1:def 2

        .= (((c1 * b1) + (c1 * (a * b3))) + (((a * c3) * b1) + ((a * c3) * (a * b3)))) by VECTSP_1:def 2

        .= ((c1 * b1) + ((c1 * (a * b3)) + (((a * c3) * b1) + ((a * c3) * (a * b3))))) by RLVECT_1:def 3

        .= ((c1 * b1) + (((c1 * (a * b3)) + ((a * c3) * b1)) + ((a * c3) * (a * b3)))) by RLVECT_1:def 3

        .= ((c1 * b1) + (((a * (c1 * b3)) + ((a * c3) * b1)) + ((a * c3) * (a * b3)))) by GROUP_1:def 3

        .= ((c1 * b1) + (((a * (c1 * b3)) + (a * (c3 * b1))) + ((a * c3) * (a * b3)))) by GROUP_1:def 3

        .= ((c1 * b1) + ((a * ((c1 * b3) + (c3 * b1))) + ((a * c3) * (a * b3)))) by VECTSP_1:def 2

        .= ((c1 * b1) + ((a * ((c1 * b3) + (c3 * b1))) + (((a * c3) * a) * b3))) by GROUP_1:def 3

        .= ((c1 * b1) + ((a * ((c1 * b3) + (c3 * b1))) + (((a * a) * c3) * b3))) by GROUP_1:def 3

        .= ((c1 * b1) + ((a * ((c1 * b3) + (c3 * b1))) + ((a * a) * (c3 * b3)))) by GROUP_1:def 3

        .= (((c1 * b1) + ((a * a) * (c3 * b3))) + (a * ((c1 * b3) + (c3 * b1)))) by RLVECT_1:def 3;

        

         E1: (c1 * b1) in { (c * b) where c,b be Element of F : c in P & b in P } by H2, H3;

        

         E2: (c3 * b3) in { (c * b) where c,b be Element of F : c in P & b in P } by H4, H5;

        (a * a) = ((a |^ 1) * a) by BINOM: 8

        .= ((a |^ 1) * (a |^ 1)) by BINOM: 8

        .= (a |^ (1 + 1)) by BINOM: 10

        .= (a ^2 ) by RING_5: 3;

        then (a * a) in P by REALALG1: 23;

        then ((a * a) * (c3 * b3)) in { (c * b) where c,b be Element of F : c in P & b in P } by E2, X;

        then

         E3: ((c1 * b1) + ((a * a) * (c3 * b3))) in { (c1 + c2) where c1,c2 be Element of F : c1 in P & c2 in P } by X, E1;

        

         E4: (c1 * b3) in { (c * b) where c,b be Element of F : c in P & b in P } by H2, H5;

        (c3 * b1) in { (c * b) where c,b be Element of F : c in P & b in P } by H4, H3;

        then ((c1 * b3) + (c3 * b1)) in { (c1 + c2) where c1,c2 be Element of F : c1 in P & c2 in P } by X, E4;

        then (a * ((c1 * b3) + (c3 * b1))) in (a * P) by X;

        hence o in S by H6, E3, X;

      end;

      P c= S by X, P1;

      then

       C: ( SQ F) c= S by X;

      now

        assume ( - ( 1. F)) in S;

        then

        consider c1,c2 be Element of F such that

         H2: ( - ( 1. F)) = (c1 + c2) & c1 in P & c2 in (a * P);

        consider c3 be Element of F such that

         H3: c2 = (a * c3) & c3 in P by H2;

        ( 0. F) = ((c1 + (a * c3)) + ( 1. F)) by H2, H3, RLVECT_1: 5

        .= ((c1 + ( 1. F)) + (a * c3)) by RLVECT_1:def 3;

        

        then

         H4: ( - (a * c3)) = (((c1 + ( 1. F)) + (a * c3)) - (a * c3))

        .= ((c1 + ( 1. F)) + ((a * c3) + ( - (a * c3)))) by RLVECT_1:def 3

        .= ((c1 + ( 1. F)) + ( 0. F)) by RLVECT_1: 5;

        c3 <> ( 0. F) by H2, H3, REALALG1: 26;

        then ((c3 " ) * c3) = ( 1. F) by VECTSP_1:def 10;

        

        then

         H5: ( - a) = (( - a) * (c3 * (c3 " )))

        .= ((( - a) * c3) * (c3 " )) by GROUP_1:def 3

        .= ((c1 + ( 1. F)) * (c3 " )) by H4, VECTSP_1: 9;

        

         H: (c1 + ( 1. F)) in { (c1 + c2) where c1,c2 be Element of F : c1 in P & c2 in P } by H2, X;

        c3 is non zero by H2, H3, REALALG1: 26;

        then (c3 " ) in P by H3, REALALG1: 27;

        then ( - a) in { (c1 * c2) where c1,c2 be Element of F : c1 in P & c2 in P } by H5, H, X;

        hence contradiction by ASS, X;

      end;

      then (S /\ ( - S)) = {( 0. F)} by C, B, REALALG1: 21;

      hence thesis by A, B, C, REALALG1:def 14;

    end;

    theorem :: REALALG2:28

    

     T1: for F be preordered Field, P be Preordering of F holds P is maximal iff P is positive_cone

    proof

      let R be preordered Field, P be Preordering of R;

      hereby

        assume

         AS: P is maximal;

        now

          let x be object;

          assume x in the carrier of R;

          then

          reconsider a = x as Element of R;

          now

            assume

             AS1: not (a in P);

            now

              assume not (( - a) in P);

              then

              reconsider Q = (P + (a * P)) as Preordering of R by T2;

              

               C: ( 0. R) in P by REALALG1: 25;

              then

               X: P = Q by AS, P1;

              ( 1. R) in P by REALALG1: 25;

              hence contradiction by P2, C, X, AS1;

            end;

            then ( - ( - a)) in ( - P);

            hence a in ( - P);

          end;

          hence x in (P \/ ( - P)) by XBOOLE_0:def 3;

        end;

        then the carrier of R c= (P \/ ( - P));

        then (P \/ ( - P)) = the carrier of R;

        then P is spanning;

        hence P is positive_cone;

      end;

      assume

       AS: P is positive_cone;

      assume not P is maximal;

      then

      consider Q be Preordering of R such that

       A: P c= Q & P <> Q;

      P c< Q by A;

      then

      consider a be object such that

       B: a in Q & not (a in P) by XBOOLE_0: 6;

      reconsider a as Element of R by B;

      a in ( - P) by AS, B, XBOOLE_0:def 3;

      then ( - a) in ( - ( - P));

      then ( - ( - a)) in ( - Q) by A;

      then a in (Q /\ ( - Q)) by B;

      then a in {( 0. R)} by REALALG1:def 7;

      then a = ( 0. R) by TARSKI:def 1;

      hence contradiction by B, REALALG1: 25;

    end;

    registration

      let F be preordered Field;

      cluster spanning -> maximal for Preordering of F;

      coherence by T1;

      cluster maximal -> spanning for Preordering of F;

      coherence

      proof

        let P be Preordering of F;

        assume P is maximal;

        then P is positive_cone by T1;

        hence thesis;

      end;

    end

    theorem :: REALALG2:29

    

     T3: for F be preordered Field, P be Preordering of F holds ex Q be Preordering of F st P c= Q & Q is maximal

    proof

      let F be preordered Field, P be Preordering of F;

      set S = { O where O be Preordering of F : P c= O };

      set R = ( RelIncl S);

      

       A2: ( field R) = S & for Y,Z be set st Y in S & Z in S holds [Y, Z] in R iff Y c= Z by WELLORD2:def 1;

      

       A3: S has_upper_Zorn_property_wrt R

      proof

        now

          let Y be set;

          assume

           AS: Y c= S & (R |_2 Y) is being_linear-order;

           H1:

          now

            let z be set;

            assume z in S;

            then

            consider p be Preordering of F such that

             H: z = p & P c= p;

            thus P c= z & z is Preordering of F by H;

          end;

          

           H2: P in S & (R |_2 Y) = (R /\ [:Y, Y:]);

          

           H3: (R |_2 Y) is connected by AS, ORDERS_1:def 6;

           H5:

          now

            let z1,z2 be set;

            assume

             HH0: z1 in Y & z2 in Y;

            per cases ;

              suppose z1 = z2;

              hence z1 c= z2 or z2 c= z1;

            end;

              suppose

               HH1: z1 <> z2;

              z1 in ( field (R |_2 Y)) & z2 in ( field (R |_2 Y)) by HH0, A2, AS, ORDERS_1: 71;

              then [z1, z2] in (R |_2 Y) or [z2, z1] in (R |_2 Y) by H3, HH1, RELAT_2:def 6, RELAT_2:def 14;

              then [z1, z2] in R or [z2, z1] in R by XBOOLE_0:def 4;

              hence z1 c= z2 or z2 c= z1 by HH0, AS, WELLORD2:def 1;

            end;

          end;

          set M = ( union Y);

          per cases ;

            suppose Y = {} ;

            then for y be set st y in Y holds [y, P] in R;

            hence ex x be set st x in S & for y be set st y in Y holds [y, x] in R by H2;

          end;

            suppose

             H: Y <> {} ;

            

             A7: M c= the carrier of F

            proof

              let o be object;

              assume o in M;

              then

              consider s be set such that

               H: o in s & s in Y by TARSKI:def 4;

              s is Preordering of F by H1, H, AS;

              hence o in the carrier of F by H;

            end;

            

             A8a: ex s be set st ( 0. F) in s & s in Y

            proof

              set s = the Element of Y;

              s in Y by H;

              then s is Preordering of F by AS, H1;

              hence thesis by H, REALALG1: 25;

            end;

            then

             A8: ( 0. F) in M by TARSKI:def 4;

            reconsider M as non empty Subset of F by A7, A8a, TARSKI:def 4;

            

             A6: M is Preordering of F

            proof

              

               A10: (M + M) c= M

              proof

                let o be object;

                assume o in (M + M);

                then

                consider a,b be Element of F such that

                 A11: o = (a + b) & a in M & b in M;

                consider sa be set such that

                 A12: a in sa & sa in Y by A11, TARSKI:def 4;

                consider sb be set such that

                 A13: b in sb & sb in Y by A11, TARSKI:def 4;

                reconsider sa, sb as Preordering of F by A12, A13, AS, H1;

                

                 A16: (sa + sa) c= sa & (sb + sb) c= sb by REALALG1:def 14;

                per cases by A12, A13, H5;

                  suppose sa c= sb;

                  then (a + b) in (sb + sb) by A12, A13;

                  hence o in M by A16, A11, A13, TARSKI:def 4;

                end;

                  suppose sb c= sa;

                  then (a + b) in (sa + sa) by A12, A13;

                  hence o in M by A16, A11, A12, TARSKI:def 4;

                end;

              end;

              

               A11: (M * M) c= M

              proof

                let o be object;

                assume o in (M * M);

                then

                consider a,b be Element of F such that

                 A11: o = (a * b) & a in M & b in M;

                consider sa be set such that

                 A12: a in sa & sa in Y by A11, TARSKI:def 4;

                consider sb be set such that

                 A13: b in sb & sb in Y by A11, TARSKI:def 4;

                reconsider sa, sb as Preordering of F by A12, A13, AS, H1;

                

                 A16: (sa * sa) c= sa & (sb * sb) c= sb by REALALG1:def 14;

                per cases by A12, A13, H5;

                  suppose sa c= sb;

                  then (a * b) in (sb * sb) by A12, A13;

                  hence o in M by A11, A13, A16, TARSKI:def 4;

                end;

                  suppose sb c= sa;

                  then (a * b) in (sa * sa) by A12, A13;

                  hence o in M by A16, A11, A12, TARSKI:def 4;

                end;

              end;

              

               A12: (M /\ ( - M)) = {( 0. F)}

              proof

                 A13:

                now

                  let o be object;

                  assume o in {( 0. F)};

                  then

                   A14: o = ( - ( 0. F)) by TARSKI:def 1;

                  then o in ( - M) by A8;

                  hence o in (M /\ ( - M)) by A14, A8;

                end;

                now

                  let o be object;

                  assume

                   A14: o in (M /\ ( - M));

                  then

                   A14a: o in M & o in ( - M) by XBOOLE_0:def 4;

                  then

                  consider so be set such that

                   A15: o in so & so in Y by TARSKI:def 4;

                  consider p be Element of F such that

                   A16: o = ( - p) & p in M by A14a;

                  consider sp be set such that

                   A17: p in sp & sp in Y by A16, TARSKI:def 4;

                  reconsider so, sp as Preordering of F by AS, A15, A17, H1;

                  reconsider o1 = o as Element of F by A14;

                  per cases by A15, A17, H5;

                    suppose

                     A19: so c= sp;

                    o in ( - sp) by A16, A17;

                    then o in (sp /\ ( - sp)) by A19, A15;

                    hence o in {( 0. F)} by REALALG1:def 14;

                  end;

                    suppose sp c= so;

                    then o in ( - so) by A16, A17;

                    then o in (so /\ ( - so)) by A15;

                    hence o in {( 0. F)} by REALALG1:def 7;

                  end;

                end;

                hence thesis by A13, TARSKI: 2;

              end;

              ( SQ F) c= M

              proof

                let o be object;

                assume

                 A13: o in ( SQ F);

                set s = the Element of Y;

                s in Y by H;

                then

                 A15: P c= s by H1, AS;

                ( SQ F) c= P by REALALG1:def 14;

                then o in s by A13, A15;

                hence o in M by H, TARSKI:def 4;

              end;

              hence thesis by A10, A11, A12, REALALG1:def 14;

            end;

            P c= M

            proof

              let o be object;

              assume

               H0: o in P;

              set s = the Element of Y;

              s in Y by H;

              then P c= s by H1, AS;

              hence o in M by H0, H, TARSKI:def 4;

            end;

            then

             A4: M in S by A6;

            now

              let y be set;

              assume

               A5: y in Y;

              then y c= M by TARSKI:def 4;

              hence [y, M] in R by AS, A4, A5, WELLORD2:def 1;

            end;

            hence ex x be set st x in S & for y be set st y in Y holds [y, x] in R by A4;

          end;

        end;

        hence thesis by ORDERS_1:def 10;

      end;

      R is_reflexive_in S & R is_transitive_in S by WELLORD2: 19, WELLORD2: 20;

      then R partially_orders S by WELLORD2: 21, ORDERS_1:def 8;

      then

      consider x be set such that

       M: x is_maximal_in R by A2, A3, ORDERS_1: 63;

      x in ( field R) by M, ORDERS_1:def 12;

      then

      consider O be Preordering of F such that

       M1: x = O & P c= O by A2;

      

       M4: O in S by M1;

      now

        let Q be Preordering of F;

        assume

         M2: O c= Q;

        then P c= Q by M1;

        then

         M5: Q in S;

        then

         M3: Q in ( field R) by WELLORD2:def 1;

         [O, Q] in R by M4, M2, M5, WELLORD2:def 1;

        hence O = Q by M3, M1, M, ORDERS_1:def 12;

      end;

      hence thesis by M1, defmax;

    end;

    registration

      cluster -> ordered for preordered Field;

      coherence

      proof

        let F be preordered Field;

        ex Q be Preordering of F st the Preordering of F c= Q & Q is maximal by T3;

        hence thesis;

      end;

    end

    theorem :: REALALG2:30

    for F be preordered Field, P be Preordering of F holds P is maximal iff P is Ordering of F;

    theorem :: REALALG2:31

    

     T1a: for F be preordered Field, P be Preordering of F holds ex O be Ordering of F st P c= O

    proof

      let F be preordered Field, P be Preordering of F;

      ex Q be Preordering of F st P c= Q & Q is maximal by T3;

      hence thesis;

    end;

    definition

      let R be ordered Ring;

      let P be Preordering of R;

      :: REALALG2:def2

      func /\ (P,R) -> Subset of R equals { x where x be Element of R : for O be Ordering of R st P c= O holds x in O };

      coherence

      proof

        now

          let x be object;

          assume x in { x where x be Element of R : for O be Ordering of R st P c= O holds x in O };

          then ex x1 be Element of R st x1 = x & for O be Ordering of R st P c= O holds x1 in O;

          hence x in the carrier of R;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    registration

      let R be ordered Ring;

      let P be Preordering of R;

      cluster ( /\ (P,R)) -> non empty;

      coherence

      proof

        for O be Ordering of R st P c= O holds ( 0. R) in O by REALALG1: 25;

        then ( 0. R) in { x where x be Element of R : for O be Ordering of R st P c= O holds x in O };

        hence thesis;

      end;

    end

    registration

      let R be ordered Ring;

      let P be Preordering of R;

      cluster ( /\ (P,R)) -> add-closed mult-closed with_squares;

      coherence

      proof

        set M = ( /\ (P,R));

        now

          let x,y be Element of R;

          assume

           AS: x in M & y in M;

          then

          consider a be Element of R such that

           A: x = a & for O be Ordering of R st P c= O holds a in O;

          consider b be Element of R such that

           B: y = b & for O be Ordering of R st P c= O holds b in O by AS;

          now

            let O be Ordering of R;

            assume P c= O;

            then a in O & b in O by A, B;

            then

             C: (a + b) in (O + O);

            (O + O) c= O by REALALG1:def 14;

            hence (a + b) in O by C;

          end;

          hence (x + y) in M by A, B;

        end;

        hence M is add-closed;

        now

          let x,y be Element of R;

          assume

           AS: x in M & y in M;

          then

          consider a be Element of R such that

           A: x = a & for O be Ordering of R st P c= O holds a in O;

          consider b be Element of R such that

           B: y = b & for O be Ordering of R st P c= O holds b in O by AS;

          now

            let O be Ordering of R;

            assume P c= O;

            then a in O & b in O by A, B;

            then

             C: (a * b) in (O * O);

            (O * O) c= O by REALALG1:def 14;

            hence (a * b) in O by C;

          end;

          hence (x * y) in M by A, B;

        end;

        hence M is mult-closed;

        

         X0: ( SQ R) c= P by REALALG1:def 14;

        now

          let o be object;

          assume

           X2: o in ( SQ R);

          then

          consider a be Element of R such that

           X1: o = a & a is square;

          for O be Ordering of R st P c= O holds a in O by X0, X1, X2;

          hence o in M by X1;

        end;

        then ( SQ R) c= M;

        hence M is with_squares;

      end;

    end

    

     s1: for F be preordered Field, P be Preordering of F holds ( /\ (P,F)) = P

    proof

      let F be preordered Field, P be Preordering of F;

      set M = ( /\ (P,F));

       A:

      now

        let o be object;

        assume

         A1: o in P;

        then

        reconsider a = o as Element of F;

        for O be Ordering of F st P c= O holds a in O by A1;

        hence o in M;

      end;

      now

        let o be object;

        assume o in M;

        then

        consider a be Element of F such that

         A: o = a & for O be Ordering of F st P c= O holds a in O;

        now

          assume

           B: not a in P;

          then not ( - ( - a)) in P;

          then

          reconsider P1 = (P + (( - a) * P)) as Preordering of F by T2;

          consider O be Ordering of F such that

           H: P1 c= O by T1a;

          

           H1: ( 0. F) in P & ( 1. F) in P by REALALG1: 25;

          then ( - a) in P1 by P2;

          then

           X: ( - ( - a)) in ( - O) by H;

          P c= P1 by H1, P1;

          then P c= O by H;

          then a in O by A;

          then a in (O /\ ( - O)) by X;

          then a in {( 0. F)} by REALALG1:def 7;

          then a = ( 0. F) by TARSKI:def 1;

          hence contradiction by B, REALALG1: 25;

        end;

        hence o in P by A;

      end;

      hence thesis by A, TARSKI: 2;

    end;

    registration

      let F be ordered Field;

      let P be Preordering of F;

      cluster ( /\ (P,F)) -> negative-disjoint;

      coherence by s1;

    end

    theorem :: REALALG2:32

    for F be ordered Field, P be Preordering of F holds ( /\ (P,F)) is Preordering of F;

    theorem :: REALALG2:33

    for F be ordered Field, P be Preordering of F holds ( /\ (P,F)) = P by s1;

    begin

    definition

      let R be Ring;

      :: REALALG2:def3

      attr R is formally_real means not ( - ( 1. R)) in ( QS R);

    end

    

     lemma1: for F be Field st F is formally_real holds (( QS F) /\ ( - ( QS F))) = {( 0. F)}

    proof

      let F be Field;

      assume

       A: F is formally_real;

      

       B: ( SQ F) c= ( QS F) by REALALG1: 18;

      (( QS F) * ( QS F)) c= ( QS F)

      proof

        let o be object;

        assume o in (( QS F) * ( QS F));

        then ex s1,s2 be Element of F st o = (s1 * s2) & s1 in ( QS F) & s2 in ( QS F);

        hence o in ( QS F) by REALALG1:def 5;

      end;

      hence thesis by A, B, REALALG1: 21;

    end;

    

     lemma2: for R be preordered non degenerated Ring holds ( QS R) <> the carrier of R

    proof

      let R be preordered non degenerated Ring;

      set P = the Preordering of R;

      ( QS R) c= P & not ( - ( 1. R)) in P by REALALG1: 26, REALALG1: 24;

      hence thesis;

    end;

    

     lemma3: for R be Field st ( Char R) <> 2 & ( QS R) <> the carrier of R holds not ( - ( 1. R)) in ( QS R)

    proof

      let R be Field;

      assume

       AS: ( Char R) <> 2 & ( QS R) <> the carrier of R;

      assume ( - ( 1. R)) in ( QS R);

      then

      consider e be Element of R such that

       H: e = ( - ( 1. R)) & e is sum_of_squares;

      now

        let a be Element of R;

        ((((a + ( 1. R)) / (2 '*' ( 1. R))) ^2 ) + (( - ( 1. R)) * (((a - ( 1. R)) / (2 '*' ( 1. R))) ^2 ))) = ((((a + ( 1. R)) / (2 '*' ( 1. R))) ^2 ) + ( - (( 1. R) * (((a - ( 1. R)) / (2 '*' ( 1. R))) ^2 )))) by VECTSP_1: 9

        .= ((((a + ( 1. R)) / (2 '*' ( 1. R))) ^2 ) - (((a - ( 1. R)) / (2 '*' ( 1. R))) ^2 ))

        .= a by AS, P5;

        hence a in ( QS R) by H;

      end;

      then the carrier of R c= ( QS R);

      hence contradiction by AS;

    end;

    theorem :: REALALG2:34

    

     T0: for F be Field st ( Char F) <> 2 holds F is formally_real iff ( QS F) is prepositive_cone

    proof

      let F be Field;

      assume

       AS: ( Char F) <> 2;

      hereby

        assume F is formally_real;

        then ( QS F) is negative-disjoint by lemma1;

        hence ( QS F) is prepositive_cone;

      end;

      assume ( QS F) is prepositive_cone;

      then F is preordered;

      hence F is formally_real by AS, lemma3, lemma2;

    end;

    theorem :: REALALG2:35

    for F be Field st ( Char F) <> 2 holds F is formally_real iff ex P be Subset of F st P is prepositive_cone

    proof

      let F be Field;

      assume

       AS: ( Char F) <> 2;

      hereby

        assume F is formally_real;

        then ( QS F) is negative-disjoint by lemma1;

        hence ex P be Subset of F st P is prepositive_cone;

      end;

      assume ex P be Subset of F st P is prepositive_cone;

      then F is preordered;

      hence F is formally_real by AS, lemma3, lemma2;

    end;

    theorem :: REALALG2:36

    

     T2: for F be Field st ( Char F) <> 2 holds F is formally_real iff ex P be Subset of F st P is positive_cone

    proof

      let F be Field;

      assume

       AS: ( Char F) <> 2;

      hereby

        assume F is formally_real;

        then ( QS F) is negative-disjoint by lemma1;

        then F is preordered;

        then F is ordered;

        hence ex P be Subset of F st P is positive_cone;

      end;

      assume ex P be Subset of F st P is positive_cone;

      then F is ordered;

      hence F is formally_real by AS, lemma3, lemma2;

    end;

    theorem :: REALALG2:37

    for F be Field st ( Char F) <> 2 holds F is formally_real iff ( QS F) <> the carrier of F by lemma3;

    registration

      cluster formally_real -> ordered for Field;

      coherence

      proof

        let F be Field;

        assume F is formally_real;

        then ( QS F) is negative-disjoint by lemma1;

        then F is preordered;

        hence thesis;

      end;

      cluster ordered -> formally_real for Field;

      coherence

      proof

        let F be Field;

        assume

         AS: F is ordered;

        then ( Char F) = 0 by REALALG1: 28;

        hence thesis by AS, T2;

      end;

    end

    registration

      cluster preordered -> formally_real for non degenerated Ring;

      coherence

      proof

        let R be non degenerated Ring;

        assume R is preordered;

        then

        reconsider R as preordered Ring;

        ( QS R) c= the Preordering of R by REALALG1: 24;

        hence thesis by REALALG1: 26;

      end;

    end

    registration

      cluster formally_real for Field;

      existence

      proof

        take F_Real ;

        thus thesis;

      end;

    end

    registration

      let F be formally_real Field;

      cluster ( QS F) -> negative-disjoint;

      coherence

      proof

        ( Char F) = 0 by REALALG1: 28;

        then ( QS F) is prepositive_cone by T0;

        hence thesis;

      end;

    end

    theorem :: REALALG2:38

    for F be formally_real Field holds ( QS F) is Preordering of F;

    theorem :: REALALG2:39

    for F be formally_real Field, a be Element of F holds (for O be Ordering of F holds a in O) iff a in ( QS F)

    proof

      let F be formally_real Field, a be Element of F;

      reconsider Q = ( QS F) as Preordering of F;

      hereby

        assume for O be Ordering of F holds a in O;

        then for O be Ordering of F st Q c= O holds a in O;

        then a in ( /\ (Q,F));

        hence a in ( QS F) by s1;

      end;

      assume

       AS: a in ( QS F);

      let O be Ordering of F;

      ( QS F) c= O by REALALG1: 24;

      hence a in O by AS;

    end;

    theorem :: REALALG2:40

    for r be Element of F_Rat st 0 <= r holds r is sum_of_squares

    proof

      let r be Element of F_Rat ;

      assume

       AS: 0 <= r;

      r in { r where r be Element of RAT : 0 <= r } by AS, GAUSSINT:def 14;

      then r in ( QS F_Rat ) by REALALG1: 38;

      then ex s be Element of F_Rat st s = r & s is sum_of_squares;

      hence thesis;

    end;

    definition

      let R be ZeroStr;

      let f be the carrier of R -valued Function;

      :: REALALG2:def4

      attr f is trivial means for i be object st i in ( dom f) holds (f . i) = ( 0. R);

    end

    definition

      let R be Ring;

      let f be non empty FinSequence of R;

      :: REALALG2:def5

      attr f is quadratic means

      : dq: for i be Element of ( dom f) holds (f . i) is square;

    end

    registration

      let R be non degenerated Ring;

      cluster <*( 1. R)*> -> quadratic non trivial;

      coherence

      proof

        set f = <*( 1. R)*>;

        1 in ( Seg 1) by FINSEQ_1: 2, TARSKI:def 1;

        then

         B: 1 in ( dom f) by FINSEQ_1: 38;

        

         D: (f . 1) = ( 1. R) by FINSEQ_1: 40;

        now

          let i be Element of ( dom f);

          ( dom f) = ( Seg 1) by FINSEQ_1: 38;

          then i = 1 by TARSKI:def 1, FINSEQ_1: 2;

          hence (f . i) is square by FINSEQ_1: 40;

        end;

        hence thesis by D, B;

      end;

    end

    registration

      let R be non degenerated Ring;

      cluster quadratic non trivial for non empty FinSequence of R;

      existence

      proof

        take <*( 1. R)*>;

        thus thesis;

      end;

    end

    theorem :: REALALG2:41

    for F be Field holds F is formally_real iff for f be quadratic non empty FinSequence of F st ( Sum f) = ( 0. F) holds f is trivial

    proof

      let F be Field;

      hereby

        assume

         AS: F is formally_real;

        now

          assume not (for f be quadratic non empty FinSequence of F st ( Sum f) = ( 0. F) holds f is trivial);

          then

          consider f be quadratic non empty FinSequence of F such that

           H1: ( Sum f) = ( 0. F) & f is non trivial;

          consider i be Element of ( dom f) such that

           H2: (f . i) <> ( 0. F) by H1;

          

           H7: ( len ( Swap (f,i,( len f)))) = ( len f) by FINSEQ_7: 18;

          then

          reconsider g = ( Swap (f,i,( len f))) as non empty FinSequence of F;

          reconsider m = (( len f) - 1) as Nat;

          reconsider p = (g | ( Seg m)) as FinSequence of F by FINSEQ_1: 18;

          (p ^ <*(f . i)*>) = g

          proof

            (m + 1) = ( len g) by FINSEQ_7: 18;

            then m <= ( len g) by NAT_1: 13;

            then

             X2: ( len p) = m & ( dom p) = ( Seg m) by FINSEQ_1: 17;

            

             X1: ( len (p ^ <*(f . i)*>)) = (( len p) + ( len <*(f . i)*>)) by FINSEQ_1: 22

            .= (m + 1) by X2, FINSEQ_1: 40

            .= ( len g) by FINSEQ_7: 18;

            now

              let k be Nat;

              assume

               X3: 1 <= k & k <= ( len g);

              per cases by XXREAL_0: 1;

                suppose

                 X4: k = ( len g);

                then (( len p) + 1) = k by X2, FINSEQ_7: 18;

                then

                 X5: ( len p) < k by NAT_1: 13;

                

                 X7: 1 <= i <= ( len f) & 1 <= ( len f) by FINSEQ_1: 20, FINSEQ_3: 25;

                

                thus ((p ^ <*(f . i)*>) . k) = ( <*(f . i)*> . (k - ( len p))) by X1, X4, X5, FINSEQ_1: 24

                .= (f . i) by X2, X4, H7, FINSEQ_1: 40

                .= (f /. i) by X7, FINSEQ_4: 15

                .= (g /. ( len f)) by X7, FINSEQ_7: 31

                .= (g . k) by X7, X4, H7, FINSEQ_4: 15;

              end;

                suppose k < ( len g);

                then (k + 1) <= ( len g) by NAT_1: 13;

                then ((k + 1) - 1) <= (( len g) - 1) by XREAL_1: 9;

                then

                 X4: k <= m by FINSEQ_7: 18;

                then k in ( dom p) by X2, X3, FINSEQ_1: 1;

                

                hence ((p ^ <*(f . i)*>) . k) = (p . k) by FINSEQ_1:def 7

                .= (g . k) by X2, X3, X4, FUNCT_1: 47, FINSEQ_1: 1;

              end;

            end;

            hence thesis by X1, FINSEQ_1: 14;

          end;

          

          then (( Sum p) + ( Sum <*(f . i)*>)) = ( Sum g) by RLVECT_1: 41

          .= ( 0. F) by H1, GROEB_2: 2;

          

          then

           H4: (( Sum p) * (( Sum <*(f . i)*>) " )) = (( - ( Sum <*(f . i)*>)) * (( Sum <*(f . i)*>) " )) by RLVECT_1: 6

          .= ( - (( Sum <*(f . i)*>) * (( Sum <*(f . i)*>) " ))) by VECTSP_1: 9

          .= ( - (( Sum <*(f . i)*>) * ((f . i) " ))) by RLVECT_1: 44

          .= ( - ((f . i) * ((f . i) " ))) by RLVECT_1: 44

          .= ( - ( 1. F)) by H2, VECTSP_1:def 10;

          

           H5: ( Sum p) in ( QS F)

          proof

            now

              let j be Nat;

              assume

               I0: j in ( dom p);

              ex k be Element of ( dom f) st (p . j) = (f . k)

              proof

                

                 I2: ( dom p) c= ( dom g) by RELAT_1: 60;

                (p . j) = (g . j) by I0, FUNCT_1: 47;

                then

                 I1: (p . j) in ( rng g) by I0, I2, FUNCT_1:def 3;

                (p . j) in ( rng f) by I1, FINSEQ_7: 22;

                then ex x be object st x in ( dom f) & (p . j) = (f . x) by FUNCT_1:def 3;

                hence thesis;

              end;

              then

              consider k be Element of ( dom f) such that

               I1: (p . j) = (f . k);

              (f . k) is square by dq;

              hence ex a be Element of F st (p . j) = (a ^2 ) by I1;

            end;

            then ( Sum p) is sum_of_squares;

            hence thesis;

          end;

          

           H6: (( Sum <*(f . i)*>) " ) in ( QS F)

          proof

            (f . i) is square by dq;

            then

            consider a be Element of F such that

             I1: (f . i) = (a ^2 );

            

             I0: a <> ( 0. F) by I1, H2;

            ((a " ) |^ 2) = ((a " ) * (a " )) by RING_5: 3

            .= ((f . i) " ) by I1, VECTSP_2: 11, I0;

            then ((f . i) " ) in ( QS F);

            hence thesis by RLVECT_1: 44;

          end;

          ( QS F) is mult-closed;

          hence contradiction by AS, H4, H5, H6;

        end;

        hence for f be quadratic non empty FinSequence of F st ( Sum f) = ( 0. F) holds f is trivial;

      end;

      assume

       AS: for f be quadratic non empty FinSequence of F st ( Sum f) = ( 0. F) holds f is trivial;

      now

        assume ( - ( 1. F)) in ( QS F);

        then

        consider e be Element of F such that

         H1: e = ( - ( 1. F)) & e is sum_of_squares;

        consider f be FinSequence of F such that

         H2: ( Sum f) = ( - ( 1. F)) & for i be Nat st i in ( dom f) holds ex a be Element of F st (f . i) = (a ^2 ) by H1;

        set g = (f ^ <*( 1. F)*>);

        

         H3: ( Sum g) = (( Sum f) + ( Sum <*( 1. F)*>)) by RLVECT_1: 41

        .= (( - ( 1. F)) + ( 1. F)) by H2, RLVECT_1: 44

        .= ( 0. F) by RLVECT_1: 5;

        

         H5b: ( len g) = (( len f) + ( len <*( 1. F)*>)) by FINSEQ_1: 22

        .= (( len f) + 1) by FINSEQ_1: 39;

        then ( len f) < ( len g) by NAT_1: 19;

        

        then

         H5: (g . ( len g)) = ( <*( 1. F)*> . (( len g) - ( len f))) by FINSEQ_1: 24

        .= ( 1. F) by H5b, FINSEQ_1: 40;

        

         H5a: 1 <= ( len g) by H5b, NAT_1: 11;

        

         H4: g is quadratic

        proof

          now

            let i be Element of ( dom g);

            

             I1: 1 <= i <= ( len g) by FINSEQ_3: 25;

            per cases ;

              suppose i = ( len g);

              hence (g . i) is square by H5;

            end;

              suppose i <> ( len g);

              then i < ((( len g) - 1) + 1) by I1, XXREAL_0: 1;

              then

               i2: i <= ( len f) by H5b, NAT_1: 13;

              then i in ( dom f) by I1, FINSEQ_3: 25;

              then (g . i) = (f . i) by FINSEQ_1:def 7;

              hence (g . i) is square by i2, H2, I1, FINSEQ_3: 25;

            end;

          end;

          hence thesis;

        end;

        g is non trivial by H5, H5a, FINSEQ_3: 25;

        hence contradiction by H3, H4, AS;

      end;

      hence F is formally_real;

    end;

    registration

      cluster -> non algebraic-closed for formally_real Field;

      coherence

      proof

        let F be formally_real Field;

        set P = the Ordering of F;

        set p = ( npoly (F,2));

        

         D: ( deg p) = 2 by RING_5: 43;

        

         A: (( deg p) + 1) = ((( len p) - 1) + 1) by HURWITZ:def 2;

        now

          assume F is algebraic-closed;

          then

          consider a be Element of F such that

           B: a is_a_root_of p by A, D, POLYNOM5:def 9, POLYNOM5:def 8;

          ( 0. F) = ( eval (p,a)) by B, POLYNOM5:def 7

          .= ((a |^ 2) - ( - ( 1. F))) by RING_5: 46;

          

          then ( - ( 1. F)) = (a |^ 2) by RLVECT_1: 21

          .= (a ^2 ) by RING_5: 3;

          then ( - ( 1. F)) in ( QS F);

          hence contradiction by REALALG1: 26;

        end;

        hence thesis;

      end;

    end

    begin

    

     lemOP: for R be preordered Ring, P be Preordering of R, a,b be Element of R holds a <= (P,b) iff a <=_ (( OrdRel P),b)

    proof

      let R be preordered Ring, P be Preordering of R;

      let a,b be Element of R;

      now

        assume a <=_ (( OrdRel P),b);

        then

        consider a1,b1 be Element of R such that

         H: [a, b] = [a1, b1] & a1 <= (P,b1);

        a = a1 & b = b1 by H, XTUPLE_0: 1;

        hence a <= (P,b) by H;

      end;

      hence thesis;

    end;

    theorem :: REALALG2:42

    

     c10a: for R be preordered Ring, P be Preordering of R, a,b be Element of R holds a <= (P,b) iff ( - b) <= (P,( - a))

    proof

      let R be preordered Ring, P be Preordering of R, a,b be Element of R;

      (( - a) - ( - b)) = (( - a) + b);

      hence thesis;

    end;

    theorem :: REALALG2:43

    

     c1: for R be preordered Ring, P be Preordering of R, a be Element of R holds a <= (P,a)

    proof

      let R be preordered Ring, P be Preordering of R;

      let a be Element of R;

      a <=_ (( OrdRel P),a) by REALALG1: 1;

      hence thesis by lemOP;

    end;

    theorem :: REALALG2:44

    

     c2: for R be preordered Ring, P be Preordering of R, a,b be Element of R st a <= (P,b) & b <= (P,a) holds a = b

    proof

      let R be preordered Ring, P be Preordering of R;

      let a,b be Element of R;

      assume a <= (P,b) & b <= (P,a);

      then a <=_ (( OrdRel P),b) & b <=_ (( OrdRel P),a);

      hence thesis by REALALG1: 2;

    end;

    theorem :: REALALG2:45

    

     c3: for R be preordered Ring, P be Preordering of R, a,b,c be Element of R st a <= (P,b) & b <= (P,c) holds a <= (P,c)

    proof

      let R be preordered Ring, P be Preordering of R;

      let a,b,c be Element of R;

      assume a <= (P,b) & b <= (P,c);

      then a <=_ (( OrdRel P),b) & b <=_ (( OrdRel P),c);

      hence thesis by lemOP, REALALG1: 3;

    end;

    theorem :: REALALG2:46

    

     c4: for R be preordered Ring, P be Preordering of R, a,b,c be Element of R st a <= (P,b) holds (a + c) <= (P,(b + c))

    proof

      let R be preordered Ring, P be Preordering of R, a,b,c be Element of R;

      assume a <= (P,b);

      then a <=_ (( OrdRel P),b);

      hence thesis by lemOP, REALALG1:def 3;

    end;

    theorem :: REALALG2:47

    

     c5: for R be preordered Ring, P be Preordering of R, a,b,c be Element of R st a <= (P,b) & ( 0. R) <= (P,c) holds (a * c) <= (P,(b * c))

    proof

      let R be preordered Ring, P be Preordering of R, a,b,c be Element of R;

      assume a <= (P,b) & ( 0. R) <= (P,c);

      then a <=_ (( OrdRel P),b) & ( 0. R) <=_ (( OrdRel P),c);

      hence thesis by lemOP, REALALG1:def 4;

    end;

    theorem :: REALALG2:48

    

     c55: for R be preordered Ring, P be Preordering of R, a,b,c be Element of R st a <= (P,b) & c <= (P,( 0. R)) holds (b * c) <= (P,(a * c))

    proof

      let R be preordered Ring, P be Preordering of R, a,b,c be Element of R;

      assume

       AS: a <= (P,b) & c <= (P,( 0. R));

      then ( - ( 0. R)) <= (P,( - c));

      then

       A: (a * ( - c)) <= (P,(b * ( - c))) by AS, c5;

      

       B: ( - (b * ( - c))) = (( - b) * ( - c)) by VECTSP_1: 9

      .= (b * c) by VECTSP_1: 10;

      ( - (a * ( - c))) = (( - a) * ( - c)) by VECTSP_1: 9

      .= (a * c) by VECTSP_1: 10;

      hence thesis by A, B, c10a;

    end;

    theorem :: REALALG2:49

    

     avb4: for R be ordered Ring, O be Ordering of R, a,b be Element of R holds a <= (O,b) or b <= (O,a)

    proof

      let R be ordered Ring, O be Ordering of R, a,b be Element of R;

      

       X: (O \/ ( - O)) = the carrier of R by REALALG1:def 8;

      assume not (a <= (O,b));

      then (b - a) in ( - O) by X, XBOOLE_0:def 3;

      then ( - (b - a)) in ( - ( - O));

      hence b <= (O,a) by RLVECT_1: 33;

    end;

    theorem :: REALALG2:50

    

     fi1: for F be preordered Field, P be Preordering of F, a,b be non zero Element of F st ( 0. F) <= (P,a) & ( 0. F) <= (P,b) holds a <= (P,b) iff (b " ) <= (P,(a " ))

    proof

      let F be preordered Field, P be Preordering of F, a,b be non zero Element of F;

      assume

       AS: ( 0. F) <= (P,a) & ( 0. F) <= (P,b);

      then

       X: ( 0. F) <= (P,(a " )) & ( 0. F) <= (P,(b " )) by REALALG1: 27;

      

       Y: a <> ( 0. F) & b <> ( 0. F);

      hereby

        assume a <= (P,b);

        then (a * (a " )) <= (P,(b * (a " ))) by X, c5;

        then ( 1. F) <= (P,(b * (a " ))) by Y, VECTSP_1:def 10;

        then (( 1. F) * (b " )) <= (P,((b * (a " )) * (b " ))) by X, c5;

        then (b " ) <= (P,(((b " ) * b) * (a " ))) by GROUP_1:def 3;

        then (b " ) <= (P,(( 1. F) * (a " ))) by Y, VECTSP_1:def 10;

        hence (b " ) <= (P,(a " ));

      end;

      assume (b " ) <= (P,(a " ));

      then ((b " ) * b) <= (P,((a " ) * b)) by AS, c5;

      then ( 1. F) <= (P,((a " ) * b)) by Y, VECTSP_1:def 10;

      then (( 1. F) * a) <= (P,(((a " ) * b) * a)) by AS, c5;

      then a <= (P,(((a " ) * a) * b)) by GROUP_1:def 3;

      then a <= (P,(( 1. F) * b)) by Y, VECTSP_1:def 10;

      hence a <= (P,b);

    end;

    theorem :: REALALG2:51

    

     fi2: for F be preordered Field, P be Preordering of F, a,b be non zero Element of F st a <= (P,( 0. F)) & b <= (P,( 0. F)) holds a <= (P,b) iff (b " ) <= (P,(a " ))

    proof

      let F be preordered Field, P be Preordering of F, a,b be non zero Element of F;

      assume

       AS: a <= (P,( 0. F)) & b <= (P,( 0. F));

      

       Y: a <> ( 0. F) & b <> ( 0. F);

      ( - a) <> ( - ( 0. F)) & ( - b) <> ( - ( 0. F));

      then ( - a) is non zero & ( - b) is non zero;

      then ( - (( - a) " )) <= (P,( - ( 0. F))) & ( - (( - b) " )) <= (P,( - ( 0. F))) by AS, REALALG1: 27;

      then

       X: (a " ) <= (P,( - ( 0. F))) & (b " ) <= (P,( - ( 0. F))) by YZ;

      hereby

        assume a <= (P,b);

        then (b * (a " )) <= (P,(a * (a " ))) by X, c55;

        then (b * (a " )) <= (P,( 1. F)) by Y, VECTSP_1:def 10;

        then (( 1. F) * (b " )) <= (P,((b * (a " )) * (b " ))) by X, c55;

        then (b " ) <= (P,(((b " ) * b) * (a " ))) by GROUP_1:def 3;

        then (b " ) <= (P,(( 1. F) * (a " ))) by Y, VECTSP_1:def 10;

        hence (b " ) <= (P,(a " ));

      end;

      assume (b " ) <= (P,(a " ));

      then ((a " ) * b) <= (P,((b " ) * b)) by AS, c55;

      then ((a " ) * b) <= (P,( 1. F)) by Y, VECTSP_1:def 10;

      then (( 1. F) * a) <= (P,(((a " ) * b) * a)) by AS, c55;

      then a <= (P,(((a " ) * a) * b)) by GROUP_1:def 3;

      then a <= (P,(( 1. F) * b)) by Y, VECTSP_1:def 10;

      hence a <= (P,b);

    end;

    definition

      let R be preordered Ring;

      let P be Preordering of R;

      let a,b be Element of R;

      :: REALALG2:def6

      pred a < P,b means a <= (P,b) & a <> b;

    end

    theorem :: REALALG2:52

    

     c20: for R be preordered non degenerated Ring, P be Preordering of R holds ( 0. R) < (P,( 1. R)) & ( - ( 1. R)) < (P,( 0. R))

    proof

      let R be preordered non degenerated Ring, P be Preordering of R;

      ( 0. R) <= (P,( 1. R)) by REALALG1: 25;

      hence ( 0. R) < (P,( 1. R));

      ( - ( 1. R)) <= (P,( 0. R)) by REALALG1: 25;

      hence ( - ( 1. R)) < (P,( 0. R));

    end;

    theorem :: REALALG2:53

    

     c10: for R be preordered Ring, P be Preordering of R, a,b be Element of R holds a < (P,b) iff ( - b) < (P,( - a)) by c10a, RLVECT_1: 18;

    theorem :: REALALG2:54

    for R be ordered Ring, O be Ordering of R, a,b be Element of R holds a < (O,b) or b < (O,a) or a = b by avb4;

    theorem :: REALALG2:55

    

     avb5: for R be preordered Ring, P be Preordering of R, a,b,c be Element of R st a < (P,b) & b <= (P,c) holds a < (P,c) by c2, c3;

    theorem :: REALALG2:56

    

     avb6: for R be preordered Ring, P be Preordering of R, a,b,c be Element of R st a <= (P,b) & b < (P,c) holds a < (P,c) by c2, c3;

    theorem :: REALALG2:57

    for R be preordered Ring, P be Preordering of R, a,b,c be Element of R st a < (P,b) holds (a + c) < (P,(b + c)) by c4, RLVECT_1: 8;

    theorem :: REALALG2:58

    for R be preordered domRing, P be Preordering of R, a,b,c be Element of R st a < (P,b) & ( 0. R) < (P,c) holds (a * c) < (P,(b * c)) by c5, GCD_1: 1;

    theorem :: REALALG2:59

    for R be preordered domRing, P be Preordering of R, a,b,c be Element of R st a < (P,b) & c < (P,( 0. R)) holds (b * c) < (P,(a * c))

    proof

      let R be preordered domRing, P be Preordering of R, a,b,c be Element of R;

      assume

       AS: a < (P,b) & c < (P,( 0. R));

      then ( - ( 0. R)) < (P,( - c)) by c10a, RLVECT_1: 18;

      then

       A: (a * ( - c)) < (P,(b * ( - c))) by AS, c5, GCD_1: 1;

      

       B: ( - (b * ( - c))) = (( - b) * ( - c)) by VECTSP_1: 9

      .= (b * c) by VECTSP_1: 10;

      ( - (a * ( - c))) = (( - a) * ( - c)) by VECTSP_1: 9

      .= (a * c) by VECTSP_1: 10;

      hence thesis by A, B, c10a, RLVECT_1: 18;

    end;

    theorem :: REALALG2:60

    for F be preordered Field, P be Preordering of F, a,b be non zero Element of F st ( 0. F) <= (P,a) & ( 0. F) <= (P,b) holds a < (P,b) iff (b " ) < (P,(a " ))

    proof

      let F be preordered Field, P be Preordering of F, a,b be non zero Element of F;

      assume

       AS: ( 0. F) <= (P,a) & ( 0. F) <= (P,b);

      

       Y: a <> ( 0. F) & b <> ( 0. F);

      (a " ) = (b " ) implies a = b

      proof

        assume (a " ) = (b " );

        then (a * (b " )) = ( 1. F) by Y, VECTSP_1:def 10;

        then ((a * (b " )) * b) = b;

        then (a * (b * (b " ))) = b by GROUP_1:def 3;

        then (a * ( 1. F)) = b by Y, VECTSP_1:def 10;

        hence a = b;

      end;

      hence thesis by AS, fi1;

    end;

    theorem :: REALALG2:61

    for F be preordered Field, P be Preordering of F, a,b be non zero Element of F st a <= (P,( 0. F)) & b <= (P,( 0. F)) holds a < (P,b) iff (b " ) < (P,(a " ))

    proof

      let F be preordered Field, P be Preordering of F, a,b be non zero Element of F;

      assume

       AS: a <= (P,( 0. F)) & b <= (P,( 0. F));

      

       Y: a <> ( 0. F) & b <> ( 0. F);

      (a " ) = (b " ) implies a = b

      proof

        assume (a " ) = (b " );

        then (a * (b " )) = ( 1. F) by Y, VECTSP_1:def 10;

        then ((a * (b " )) * b) = b;

        then (a * (b * (b " ))) = b by GROUP_1:def 3;

        then (a * ( 1. F)) = b by Y, VECTSP_1:def 10;

        hence a = b;

      end;

      hence thesis by AS, fi2;

    end;

    definition

      let R be preordered Ring;

      let P be Preordering of R;

      let a be Element of R;

      :: REALALG2:def7

      attr a is P -ordered means

      : defppp: a in (P \/ ( - P));

      :: REALALG2:def8

      attr a is P -positive means a in (P \ {( 0. R)});

      :: REALALG2:def9

      attr a is P -negative means

      : defn: a in (( - P) \ {( 0. R)});

    end

    registration

      let R be preordered Ring;

      let P be Preordering of R;

      cluster P -ordered for Element of R;

      existence

      proof

        take ( 1. R);

        ( 1. R) in P by REALALG1: 25;

        hence thesis by XBOOLE_0:def 3;

      end;

    end

    registration

      let R be preordered Ring;

      let P be Preordering of R;

      cluster P -positive -> P -ordered for Element of R;

      coherence

      proof

        let a be Element of R;

        assume a is P -positive;

        then a in P by XBOOLE_0:def 5;

        hence a in (P \/ ( - P)) by XBOOLE_0:def 3;

      end;

      cluster P -negative -> P -ordered for Element of R;

      coherence

      proof

        let a be Element of R;

        assume a is P -negative;

        then a in ( - P) by XBOOLE_0:def 5;

        hence a in (P \/ ( - P)) by XBOOLE_0:def 3;

      end;

    end

    registration

      let R be preordered non degenerated Ring;

      let P be Preordering of R;

      cluster P -positive for Element of R;

      existence

      proof

        take ( 1. R);

        ( 1. R) in P & not ( 1. R) in {( 0. R)} by REALALG1: 25, TARSKI:def 1;

        hence thesis by XBOOLE_0:def 5;

      end;

      cluster P -negative for Element of R;

      existence

      proof

        take ( - ( 1. R));

        ( - ( - ( 1. R))) <> ( - ( 0. R));

        then ( 1. R) in P & ( - ( 1. R)) <> ( 0. R) by REALALG1: 25;

        then ( - ( 1. R)) in ( - P) & not ( - ( 1. R)) in {( 0. R)} by TARSKI:def 1;

        hence thesis by XBOOLE_0:def 5;

      end;

      cluster non P -positive for Element of R;

      existence

      proof

        take ( 0. R);

        ( 0. R) in {( 0. R)} by TARSKI:def 1;

        hence thesis by XBOOLE_0:def 5;

      end;

      cluster non P -negative for Element of R;

      existence

      proof

        take ( 0. R);

        ( 0. R) in {( 0. R)} by TARSKI:def 1;

        hence thesis by XBOOLE_0:def 5;

      end;

    end

    

     x1: for R be preordered Ring, P be Preordering of R, a be Element of R holds a is P -positive iff ( 0. R) < (P,a)

    proof

      let R be preordered Ring, P be Preordering of R, a be Element of R;

      hereby

        assume a is P -positive;

        then a in P & not a in {( 0. R)} by XBOOLE_0:def 5;

        then ( 0. R) <= (P,a) & a <> ( 0. R) by TARSKI:def 1;

        hence ( 0. R) < (P,a);

      end;

      assume ( 0. R) < (P,a);

      then ( 0. R) <= (P,a) & a <> ( 0. R);

      then a in P & not a in {( 0. R)} by TARSKI:def 1;

      hence a is P -positive by XBOOLE_0:def 5;

    end;

    

     x2: for R be preordered Ring, P be Preordering of R, a be Element of R holds a is P -negative iff a < (P,( 0. R))

    proof

      let R be preordered Ring, P be Preordering of R, a be Element of R;

      hereby

        assume a is P -negative;

        then a in ( - P) & not a in {( 0. R)} by XBOOLE_0:def 5;

        then ( - a) in ( - ( - P)) & not a in {( 0. R)};

        then a <= (P,( 0. R)) & a <> ( 0. R) by TARSKI:def 1;

        hence a < (P,( 0. R));

      end;

      assume a < (P,( 0. R));

      then a <= (P,( 0. R)) & a <> ( 0. R);

      then ( - ( - a)) in ( - P) & not a in {( 0. R)} by TARSKI:def 1;

      hence a is P -negative by XBOOLE_0:def 5;

    end;

    registration

      let R be preordered non degenerated Ring;

      let P be Preordering of R;

      cluster P -positive -> non zero non P -negative for Element of R;

      coherence

      proof

        let a be Element of R;

        assume a is P -positive;

        then

         A: ( 0. R) < (P,a) by x1;

        then

         B: ( 0. R) <= (P,a);

        now

          assume a in (( - P) \ {( 0. R)});

          then a is P -negative;

          then ( - ( 0. R)) < (P,( - a)) by x2, c10;

          then ( 0. R) <= (P,( - a));

          then ( - ( - a)) in ( - P);

          then a in (P /\ ( - P)) by B;

          then a in {( 0. R)} by REALALG1:def 7;

          hence contradiction by A, TARSKI:def 1;

        end;

        hence thesis by A;

      end;

      cluster P -negative -> non zero non P -positive for Element of R;

      coherence

      proof

        let a be Element of R;

        assume a is P -negative;

        then

         A: a < (P,( 0. R)) by x2;

        then a <= (P,( 0. R));

        then

         B: ( - ( - a)) in ( - P);

        now

          assume a in (P \ {( 0. R)});

          then a is P -positive;

          then ( 0. R) < (P,a) by x1;

          then ( 0. R) <= (P,a);

          then a in (P /\ ( - P)) by B;

          then a in {( 0. R)} by REALALG1:def 7;

          hence contradiction by A, TARSKI:def 1;

        end;

        hence thesis by A;

      end;

    end

    registration

      let R be preordered non degenerated Ring;

      let P be Preordering of R;

      let a be P -ordered Element of R;

      cluster ( - a) -> P -ordered;

      coherence

      proof

        a in (P \/ ( - P)) by defppp;

        then ( - a) in ( - (P \/ ( - P)));

        then ( - a) in (( - P) \/ ( - ( - P))) by REALALG1: 16;

        hence thesis;

      end;

    end

    

     lemsqf: for F be preordered Field, P be Preordering of F, a be non zero Element of F holds a in (P \/ ( - P)) iff (a " ) in (P \/ ( - P))

    proof

      let F be preordered Field, P be Preordering of F, a be non zero Element of F;

      ( - a) <> ( - ( 0. F));

      then

       X: (a " ) is non zero & ( - (a " )) is non zero & ( - a) is non zero by VECTSP_1: 25;

      hereby

        assume a in (P \/ ( - P));

        per cases by XBOOLE_0:def 3;

          suppose a in P;

          then (a " ) in P by REALALG1: 27;

          hence (a " ) in (P \/ ( - P)) by XBOOLE_0:def 3;

        end;

          suppose a in ( - 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;

        end;

      end;

      assume (a " ) in (P \/ ( - P));

      per cases by XBOOLE_0:def 3;

        suppose (a " ) in P;

        then ((a " ) " ) in P by X, REALALG1: 27;

        hence a in (P \/ ( - P)) by XBOOLE_0:def 3;

      end;

        suppose (a " ) in ( - 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;

      end;

    end;

    registration

      let F be Field;

      let a be non zero Element of F;

      cluster (a " ) -> non zero;

      coherence

      proof

        

         A: a <> ( 0. F);

        assume (a " ) is zero;

        

        then ( 0. F) = (a * (a " ))

        .= ( 1. F) by A, VECTSP_1:def 10;

        hence contradiction;

      end;

    end

    registration

      let F be preordered Field;

      let P be Preordering of F;

      let a be non zeroP -ordered Element of F;

      cluster (a " ) -> P -ordered;

      coherence by defppp, lemsqf;

    end

    registration

      let R be ordered non degenerated Ring;

      let O be Ordering of R;

      cluster non zero non O -positive -> O -negative for Element of R;

      coherence

      proof

        let a be Element of R;

        assume

         A: a is non zero non O -positive;

        then a <> ( 0. R) & not (( 0. R) < (O,a)) by x1;

        then a < (O,( 0. R)) or a = ( 0. R) by avb4;

        hence thesis by A, x2;

      end;

      cluster non zero non O -negative -> O -positive for Element of R;

      coherence ;

    end

    theorem :: REALALG2:62

    for R be preordered Ring, P be Preordering of R, a be Element of R holds a is P -positive iff ( 0. R) < (P,a) by x1;

    theorem :: REALALG2:63

    for R be preordered Ring, P be Preordering of R, a be Element of R holds a is P -negative iff a < (P,( 0. R)) by x2;

    theorem :: REALALG2:64

    

     x1a: for R be preordered Ring, P be Preordering of R holds for a be P -ordered Element of R holds a is non P -negative iff ( 0. R) <= (P,a)

    proof

      let R be preordered Ring, P be Preordering of R;

      let a be P -ordered Element of R;

      

       H: a in (P \/ ( - P)) & (P /\ ( - P)) = {( 0. R)} by REALALG1:def 14, defppp;

      hereby

        assume a is non P -negative;

        per cases by XBOOLE_0:def 5;

          suppose not a in ( - P);

          hence ( 0. R) <= (P,a) by H, XBOOLE_0:def 3;

        end;

          suppose a in {( 0. R)};

          then a = ( 0. R) by TARSKI:def 1;

          hence ( 0. R) <= (P,a) by c1;

        end;

      end;

      assume

       C: ( 0. R) <= (P,a);

      per cases ;

        suppose a = ( 0. R);

        then a in {( 0. R)} by TARSKI:def 1;

        hence a is non P -negative by XBOOLE_0:def 5;

      end;

        suppose

         D: a <> ( 0. R);

        now

          assume a in ( - P);

          then a in {( 0. R)} by C, H;

          hence contradiction by D, TARSKI:def 1;

        end;

        hence a is non P -negative by XBOOLE_0:def 5;

      end;

    end;

    theorem :: REALALG2:65

    for R be preordered Ring, P be Preordering of R holds for a be P -ordered Element of R holds a is non P -positive iff a <= (P,( 0. R))

    proof

      let R be preordered Ring, P be Preordering of R;

      let a be P -ordered Element of R;

      

       H: a in (P \/ ( - P)) & (P /\ ( - P)) = {( 0. R)} by REALALG1:def 14, defppp;

      hereby

        assume a is non P -positive;

        per cases by XBOOLE_0:def 5;

          suppose not a in P;

          then a in ( - P) by H, XBOOLE_0:def 3;

          then ( - a) in ( - ( - P));

          hence a <= (P,( 0. R));

        end;

          suppose a in {( 0. R)};

          then a = ( 0. R) by TARSKI:def 1;

          hence a <= (P,( 0. R)) by c1;

        end;

      end;

      assume a <= (P,( 0. R));

      then

       C: ( - ( - a)) in ( - P);

      per cases ;

        suppose a = ( 0. R);

        then a in {( 0. R)} by TARSKI:def 1;

        hence a is non P -positive by XBOOLE_0:def 5;

      end;

        suppose

         D: a <> ( 0. R);

        now

          assume a in P;

          then a in {( 0. R)} by C, H;

          hence contradiction by D, TARSKI:def 1;

        end;

        hence a is non P -positive by XBOOLE_0:def 5;

      end;

    end;

    begin

    definition

      let R be preordered Ring;

      let P be Preordering of R;

      let a be Element of R;

      :: REALALG2:def10

      func absolute_value (P,a) -> Element of R equals

      : defa: a if a in P,

( - a) if a in ( - P)

      otherwise ( - ( 1. R));

      coherence ;

      consistency

      proof

        let r be Element of R;

        thus (a in P & a in ( - P)) implies (r = a iff r = ( - a))

        proof

          assume a in P & a in ( - P);

          then

           A: a in (P /\ ( - P));

          (P /\ ( - P)) = {( 0. R)} by REALALG1:def 14;

          then a = ( 0. R) by A, TARSKI:def 1;

          hence thesis;

        end;

      end;

    end

    definition

      let R be ordered Ring;

      let O be Ordering of R;

      let a be Element of R;

      :: original: absolute_value

      redefine

      :: REALALG2:def11

      func absolute_value (O,a) -> Element of R equals a if a in O

      otherwise ( - a);

      coherence ;

      consistency ;

      compatibility

      proof

        let r be Element of R;

        thus a in O implies (r = ( absolute_value (O,a)) iff r = a) by defa;

        thus not (a in O) implies (r = ( absolute_value (O,a)) iff r = ( - a))

        proof

          assume

           AS: not (a in O);

          (O \/ ( - O)) = the carrier of R by REALALG1:def 8;

          then a in ( - O) by AS, XBOOLE_0:def 3;

          hence thesis by defa;

        end;

      end;

    end

    notation

      let R be preordered Ring;

      let P be Preordering of R;

      let a be Element of R;

      synonym abs (P,a) for absolute_value (P,a);

    end

    theorem :: REALALG2:66

    

     av0: for R be preordered non degenerated Ring, P be Preordering of R, a be Element of R holds ( 0. R) <= (P,( abs (P,a))) iff a is P -ordered

    proof

      let R be preordered non degenerated Ring, O be Preordering of R, a be Element of R;

      hereby

        assume ( 0. R) <= (O,( abs (O,a)));

        then

         C: ( - ( 1. R)) < (O,( abs (O,a))) by avb5, c20;

        per cases ;

          suppose a in O;

          hence a is O -ordered by XBOOLE_0:def 3;

        end;

          suppose a in ( - O);

          hence a is O -ordered by XBOOLE_0:def 3;

        end;

          suppose not (a in O) & not (a in ( - O));

          hence a is O -ordered by C, defa;

        end;

      end;

      assume a is O -ordered;

      per cases by XBOOLE_0:def 3;

        suppose a in O;

        hence ( 0. R) <= (O,( abs (O,a))) by defa;

      end;

        suppose

         D: a in ( - O);

        then ( - a) in ( - ( - O));

        hence ( 0. R) <= (O,( abs (O,a))) by D, defa;

      end;

    end;

    theorem :: REALALG2:67

    

     av00: for R be preordered non degenerated Ring, P be Preordering of R, a be Element of R holds not a is P -ordered iff ( abs (P,a)) = ( - ( 1. R))

    proof

      let R be preordered non degenerated Ring, P be Preordering of R, a be Element of R;

      hereby

        assume not a is P -ordered;

        then not (a in P) & not (a in ( - P)) by XBOOLE_0:def 3;

        hence ( abs (P,a)) = ( - ( 1. R)) by defa;

      end;

      assume

       AS: ( abs (P,a)) = ( - ( 1. R));

      assume a is P -ordered;

      then ( 0. R) <= (P,( abs (P,a))) by av0;

      hence contradiction by AS, REALALG1: 26;

    end;

    theorem :: REALALG2:68

    for R be preordered non degenerated Ring, P be Preordering of R, a be Element of R holds ( abs (P,a)) = ( 0. R) iff a = ( 0. R)

    proof

      let R be preordered non degenerated Ring, O be Preordering of R, a be Element of R;

      hereby

        assume

         B: ( abs (O,a)) = ( 0. R);

        now

          assume ( abs (O,a)) = ( - ( 1. R));

          then (( - ( 1. R)) + ( 1. R)) = (( 0. R) + ( 1. R)) by B;

          hence contradiction by RLVECT_1: 5;

        end;

        then

         C: a is O -ordered by av00;

        per cases ;

          suppose a in O;

          hence a = ( 0. R) by B, defa;

        end;

          suppose not a in O;

          then a in ( - O) by C, XBOOLE_0:def 3;

          then ( - a) = ( 0. R) by B, defa;

          then ( - ( - a)) = ( 0. R);

          hence a = ( 0. R);

        end;

      end;

      thus thesis by REALALG1: 25, defa;

    end;

    theorem :: REALALG2:69

    

     av2: for R be preordered domRing, P be Preordering of R, a be Element of R holds ( abs (P,a)) = a iff ( 0. R) <= (P,a)

    proof

      let R be preordered domRing, O be Preordering of R, a be Element of R;

      hereby

        assume

         B: ( abs (O,a)) = a;

        per cases ;

          suppose a in O;

          hence ( 0. R) <= (O,a);

        end;

          suppose a in ( - O);

          then a = ( - a) by B, defa;

          then a = ( 0. R) by tA;

          hence ( 0. R) <= (O,a) by c1;

        end;

          suppose

           D: not (a in O) & not (a in ( - O));

          then ( - a) = ( - ( - ( 1. R))) by B, defa;

          then ( - a) in O by REALALG1: 25;

          then ( - ( - a)) in ( - O);

          hence ( 0. R) <= (O,a) by D;

        end;

      end;

      thus thesis by defa;

    end;

    theorem :: REALALG2:70

    

     av3: for R be preordered domRing, P be Preordering of R, a be Element of R holds ( abs (P,a)) = ( - a) iff a <= (P,( 0. R))

    proof

      let R be preordered domRing, O be Preordering of R, a be Element of R;

      hereby

        assume

         B: ( abs (O,a)) = ( - a);

        per cases ;

          suppose a in ( - O);

          then ( - a) in ( - ( - O));

          hence a <= (O,( 0. R));

        end;

          suppose a in O;

          hence a <= (O,( 0. R)) by B, defa;

        end;

          suppose

           D: not (a in O) & not (a in ( - O));

          then ( - ( - a)) = ( - ( - ( 1. R))) by B, defa;

          hence a <= (O,( 0. R)) by D, REALALG1: 25;

        end;

      end;

      assume a <= (O,( 0. R));

      then ( - ( - a)) in ( - O);

      hence ( abs (O,a)) = ( - a) by defa;

    end;

    theorem :: REALALG2:71

    for R be preordered Ring, P be Preordering of R, a be Element of R holds ( abs (P,a)) = ( abs (P,( - a)))

    proof

      let R be preordered Ring, O be Preordering of R, a be Element of R;

      per cases ;

        suppose

         D: a in ( - O);

        then

         E: ( abs (O,a)) = ( - a) by defa;

        ( - a) in ( - ( - O)) by D;

        hence ( abs (O,a)) = ( abs (O,( - a))) by E, defa;

      end;

        suppose

         D: a in O;

        then

         E: ( abs (O,a)) = a by defa;

        ( - a) in ( - O) & ( - ( - a)) = a by D;

        hence ( abs (O,a)) = ( abs (O,( - a))) by E, defa;

      end;

        suppose

         D: not (a in O) & not (a in ( - O));

        then

         E: ( abs (O,a)) = ( - ( 1. R)) by defa;

         not (( - a) in O) & not (( - a) in ( - O))

        proof

          assume ( - a) in O or ( - a) in ( - O);

          then ( - ( - a)) in ( - O) or ( - ( - a)) in ( - ( - O));

          hence contradiction by D;

        end;

        hence ( abs (O,a)) = ( abs (O,( - a))) by E, defa;

      end;

    end;

    theorem :: REALALG2:72

    for R be preordered non degenerated Ring, P be Preordering of R, a be Element of R holds ( - ( abs (P,a))) <= (P,a) & a <= (P,( abs (P,a))) iff a is P -ordered

    proof

      let R be preordered non degenerated Ring, O be Preordering of R, a be Element of R;

      hereby

        assume

         AS: ( - ( abs (O,a))) <= (O,a) & a <= (O,( abs (O,a)));

        per cases ;

          suppose a in ( - O);

          hence a is O -ordered by XBOOLE_0:def 3;

        end;

          suppose a in O;

          hence a is O -ordered by XBOOLE_0:def 3;

        end;

          suppose not (a in O) & not (a in ( - O));

          then ( 1. R) <= (O,a) & a <= (O,( - ( 1. R))) by AS, defa;

          then

           F: ( 1. R) <= (O,( - ( 1. R))) by c3;

          ( - ( 1. R)) < (O,( 0. R)) by c20;

          then ( - ( 1. R)) < (O,( 1. R)) by c20, avb6;

          hence a is O -ordered by F, c2;

        end;

      end;

      assume

       G: a is O -ordered;

      

       Y: ( 0. R) <= (O,( abs (O,a))) by G, av0;

      then

       X: ( abs (O,a)) in O & (O + O) c= O by REALALG1:def 14;

      per cases by G, XBOOLE_0:def 3;

        suppose

         A: a in O;

        then

         C: ( abs (O,a)) = a by defa;

        then

         B: (( abs (O,a)) - a) = ( 0. R) by RLVECT_1: 15;

        (a + ( abs (O,a))) in (O + O) by C, A;

        hence ( - ( abs (O,a))) <= (O,a) by X;

        thus a <= (O,( abs (O,a))) by B, REALALG1: 25;

      end;

        suppose

         A: a in ( - O);

        then ( abs (O,a)) = ( - a) by defa;

        then (( abs (O,a)) - ( - a)) = ( 0. R) by RLVECT_1: 15;

        then (( abs (O,a)) + a) in O by REALALG1: 25;

        hence ( - ( abs (O,a))) <= (O,a);

        ( - a) in ( - ( - O)) by A;

        then (( abs (O,a)) + ( - a)) in (O + O) by Y;

        hence a <= (O,( abs (O,a))) by X;

      end;

    end;

    theorem :: REALALG2:73

    

     sq2: for F be preordered Field, P be Preordering of F, a be non zeroP -ordered Element of F holds ( abs (P,(a " ))) = (( abs (P,a)) " )

    proof

      let F be preordered Field, P be Preordering of F, a be non zeroP -ordered Element of F;

      

       AS: a in (P \/ ( - P)) by defppp;

      

       Y: a <> ( 0. F);

      ( - a) <> ( - ( 0. F));

      then

       X: (a " ) is non zero & ( - (a " )) is non zero & ( - a) is non zero;

      (( abs (P,(a " ))) * ( abs (P,a))) = ( 1_ F)

      proof

        per cases by AS, XBOOLE_0:def 3;

          suppose

           K: a in P;

          then ( 0. F) <= (P,a);

          then

           L: ( abs (P,a)) = a by av2;

          ( 0. F) <= (P,(a " )) by K, REALALG1: 27;

          then ( abs (P,(a " ))) = (a " ) by av2;

          hence (( abs (P,(a " ))) * ( abs (P,a))) = ( 1_ F) by Y, L, VECTSP_2: 9;

        end;

          suppose a in ( - P);

          then

           K: ( - a) in ( - ( - P));

          then ( - ( - a)) <= (P,( 0. F));

          then

           L: ( abs (P,a)) = ( - a) by av3;

          ( - (( - a) " )) <= (P,( 0. F)) by K, X, REALALG1: 27;

          then (a " ) <= (P,( 0. F)) by YZ;

          then ( abs (P,(a " ))) = ( - (a " )) by av3;

          

          hence (( abs (P,(a " ))) * ( abs (P,a))) = ((a " ) * a) by L, VECTSP_1: 10

          .= ( 1_ F) by Y, VECTSP_2: 9;

        end;

      end;

      hence thesis by VECTSP_2: 10;

    end;

    theorem :: REALALG2:74

    for R be preordered Ring, P be Preordering of R, a,b be Element of R holds ( abs (P,(a - b))) = ( abs (P,(b - a)))

    proof

      let R be preordered Ring, O be Preordering of R, a,b be Element of R;

      per cases ;

        suppose

         A: (a - b) in O;

        then ( - (a - b)) in ( - O);

        then (b - a) in ( - O) by RLVECT_1: 33;

        

        hence ( abs (O,(b - a))) = ( - (b - a)) by defa

        .= (a - b) by RLVECT_1: 33

        .= ( abs (O,(a - b))) by A, defa;

      end;

        suppose

         A: (a - b) in ( - O);

        then ( - (a - b)) in ( - ( - O));

        then

         B: (b - a) in O by RLVECT_1: 33;

        

        thus ( abs (O,(a - b))) = ( - (a - b)) by A, defa

        .= (b - a) by RLVECT_1: 33

        .= ( abs (O,(b - a))) by B, defa;

      end;

        suppose

         A: not ((a - b) in O) & not ((a - b) in ( - O));

        then

         B: ( abs (O,(a - b))) = ( - ( 1. R)) by defa;

         not ((b - a) in O) & not ((b - a) in ( - O))

        proof

          assume (b - a) in O or (b - a) in ( - O);

          then ( - (b - a)) in ( - O) or ( - (b - a)) in ( - ( - O));

          hence contradiction by A, RLVECT_1: 33;

        end;

        hence ( abs (O,(a - b))) = ( abs (O,(b - a))) by B, defa;

      end;

    end;

    theorem :: REALALG2:75

    

     ineq2: for R be preordered non degenerated Ring, P be Preordering of R, a be Element of R holds (( - ( abs (P,a))) <= (P,a) & a <= (P,( abs (P,a)))) iff a is P -ordered

    proof

      let R be preordered non degenerated Ring, P be Preordering of R, a be Element of R;

      hereby

        assume

         AS: ( - ( abs (P,a))) <= (P,a) & a <= (P,( abs (P,a)));

        now

          assume not a is P -ordered;

          then

           B: ( - ( - ( 1. R))) <= (P,a) & a <= (P,( - ( 1. R))) by AS, av00;

          ( 0. R) < (P,( 1. R)) & ( - ( 1. R)) < (P,( 0. R)) by c20;

          then ( - ( 1. R)) < (P,( 1. R)) by c2, c3;

          then a < (P,( 1. R)) by B, c2, c3;

          hence contradiction by B, c2;

        end;

        hence a is P -ordered;

      end;

      

       X: (P + P) c= P by REALALG1:def 14;

      now

        assume a in (P \/ ( - P));

        per cases by XBOOLE_0:def 3;

          suppose

           A: a in P;

          then

           B: ( abs (P,a)) = a by defa;

          then (a + ( abs (P,a))) in (P + P) by A;

          hence ( - ( abs (P,a))) <= (P,a) & a <= (P,( abs (P,a))) by X, B, c1;

        end;

          suppose a in ( - P);

          then

           A1: ( abs (P,a)) = ( - a) & ( - a) in ( - ( - P)) by defa;

          then

           B: ( - ( abs (P,a))) = ( - ( - a)) & ( - a) in P;

          (( abs (P,a)) + ( - a)) in (P + P) by A1;

          hence ( - ( abs (P,a))) <= (P,a) & a <= (P,( abs (P,a))) by X, B, c1;

        end;

      end;

      hence thesis;

    end;

    theorem :: REALALG2:76

    

     abs10: for R be preordered non degenerated Ring, P be Preordering of R, a,b be P -ordered Element of R holds ( abs (P,(a * b))) = (( abs (P,a)) * ( abs (P,b)))

    proof

      let R be preordered non degenerated Ring, P be Preordering of R, a,b be P -ordered Element of R;

      

       AS: (a in (P \/ ( - P)) & b in (P \/ ( - P))) by defppp;

      

       X: (P * P) c= P by REALALG1:def 14;

      

       Y: (( - P) * P) c= ( - P) & (P * ( - P)) c= ( - P) by v2;

      

       Z: (( - P) * ( - P)) c= P by v1;

      per cases by AS, XBOOLE_0:def 3;

        suppose

         A: a in P;

        per cases by AS, XBOOLE_0:def 3;

          suppose

           A1: b in P;

          then

           B: ( abs (P,a)) = a & ( abs (P,b)) = b by A, defa;

          (a * b) in (P * P) by A, A1;

          hence (( abs (P,a)) * ( abs (P,b))) = ( abs (P,(a * b))) by X, defa, B;

        end;

          suppose

           A1: b in ( - P);

          then

           B: ( abs (P,a)) = a & ( abs (P,b)) = ( - b) by A, defa;

          

           C: (a * b) in (P * ( - P)) by A, A1;

          

          thus (( abs (P,a)) * ( abs (P,b))) = ( - (a * b)) by VECTSP_1: 8, B

          .= ( abs (P,(a * b))) by C, Y, defa;

        end;

      end;

        suppose

         A: a in ( - P);

        per cases by AS, XBOOLE_0:def 3;

          suppose

           A1: b in ( - P);

          then

           B: ( abs (P,a)) = ( - a) & ( abs (P,b)) = ( - b) by A, defa;

          

           C: (a * b) in (( - P) * ( - P)) by A, A1;

          

          thus (( abs (P,a)) * ( abs (P,b))) = (a * b) by VECTSP_1: 10, B

          .= ( abs (P,(a * b))) by C, Z, defa;

        end;

          suppose

           A1: b in P;

          then

           B: ( abs (P,a)) = ( - a) & ( abs (P,b)) = b by A, defa;

          

           C: (a * b) in (( - P) * P) by A, A1;

          

          thus (( abs (P,a)) * ( abs (P,b))) = ( - (a * b)) by VECTSP_1: 9, B

          .= ( abs (P,(a * b))) by C, Y, defa;

        end;

      end;

    end;

    theorem :: REALALG2:77

    for F be preordered Field, P be Preordering of F holds for a be non zeroP -ordered Element of F, b be P -ordered Element of F holds ( abs (P,(b * (a " )))) = (( abs (P,b)) * (( abs (P,a)) " ))

    proof

      let F be preordered Field, P be Preordering of F, a be non zeroP -ordered Element of F, b be P -ordered Element of F;

      

      thus ( abs (P,(b * (a " )))) = (( abs (P,b)) * ( abs (P,(a " )))) by abs10

      .= (( abs (P,b)) * (( abs (P,a)) " )) by sq2;

    end;

    theorem :: REALALG2:78

    

     ineq1: for R be preordered domRing, P be Preordering of R, a be P -ordered Element of R, p be P -ordered non P -negative Element of R holds ( abs (P,a)) <= (P,p) iff (( - p) <= (P,a) & a <= (P,p))

    proof

      let R be preordered domRing, P be Preordering of R, a be P -ordered Element of R, p be P -ordered non P -negative Element of R;

      

       H: not (p in (( - P) \ {( 0. R)})) & p in (P \/ ( - P)) by defn, defppp;

      then not (p in ( - P)) or p in {( 0. R)} by XBOOLE_0:def 5;

      then

       As: not (p in ( - P)) or p = ( 0. R) by TARSKI:def 1;

      then

       AS: a in (P \/ ( - P)) & ( 0. R) <= (P,p) by defppp, H, XBOOLE_0:def 3, REALALG1: 25;

      hereby

        assume

         A1: ( abs (P,a)) <= (P,p);

        per cases by AS, XBOOLE_0:def 3;

          suppose a in P;

          then

           A2: ( 0. R) <= (P,a);

          

           A3: a <= (P,( abs (P,a))) by ineq2;

          ( - p) <= (P,( 0. R)) by As, H, XBOOLE_0:def 3, REALALG1: 25;

          hence ( - p) <= (P,a) & a <= (P,p) by A3, A2, A1, c3;

        end;

          suppose a in ( - P);

          then ( - a) in ( - ( - P));

          then

           A3: ( - ( - a)) <= (P,( 0. R));

          ( - ( abs (P,a))) <= (P,a) by ineq2;

          then ( - a) <= (P,( - ( - ( abs (P,a))))) by c10a;

          then ( - a) <= (P,p) by A1, c3;

          hence ( - p) <= (P,a) & a <= (P,p) by A3, AS, c3, c10a;

        end;

      end;

      assume

       A1: ( - p) <= (P,a) & a <= (P,p);

      per cases by AS, XBOOLE_0:def 3;

        suppose a in P;

        then ( 0. R) <= (P,a);

        hence ( abs (P,a)) <= (P,p) by A1, av2;

      end;

        suppose a in ( - P);

        then ( - a) in ( - ( - P));

        then ( - ( - a)) <= (P,( 0. R));

        then ( abs (P,a)) = ( - a) by av3;

        hence ( abs (P,a)) <= (P,p) by A1, c10a;

      end;

    end;

    theorem :: REALALG2:79

    for R be preordered domRing, P be Preordering of R, a,b be P -ordered Element of R holds ( abs (P,(a + b))) <= (P,(( abs (P,a)) + ( abs (P,b))))

    proof

      let R be preordered domRing, P be Preordering of R, a,b be P -ordered Element of R;

      

       A1: ( 0. R) <= (P,( abs (P,b))) by av0;

      (( 0. R) + ( abs (P,b))) <= (P,(( abs (P,a)) + ( abs (P,b)))) by c4, av0;

      then

       A: ( 0. R) <= (P,(( abs (P,a)) + ( abs (P,b)))) by c3, A1;

      per cases ;

        suppose (a + b) is non P -ordered;

        then not ((a + b) in P) & not (a + b) in ( - P) by XBOOLE_0:def 3;

        then

         B: ( abs (P,(a + b))) = ( - ( 1. R)) by defa;

        ( - ( 1. R)) < (P,( 0. R)) by c20;

        hence thesis by B, A, c3;

      end;

        suppose

         AS1: (a + b) is P -ordered;

        now

          assume (( abs (P,a)) + ( abs (P,b))) is P -negative;

          then ( - ( 0. R)) < (P,( - (( abs (P,a)) + ( abs (P,b))))) by x2, c10;

          then (( 0. R) + (( abs (P,a)) + ( abs (P,b)))) < (P,(( - (( abs (P,a)) + ( abs (P,b)))) + (( abs (P,a)) + ( abs (P,b))))) by c4, RLVECT_1: 8;

          then (( 0. R) + ( 0. R)) < (P,((( abs (P,a)) + ( abs (P,b))) + ( - (( abs (P,a)) + ( abs (P,b)))))) by A, c2, c3;

          hence contradiction by RLVECT_1: 5;

        end;

        then

         A1: (( abs (P,a)) + ( abs (P,b))) is P -ordered non P -negative by A, XBOOLE_0:def 3;

        

         B: ( - (( abs (P,a)) + ( abs (P,b)))) <= (P,(a + b))

        proof

          ( - ( abs (P,a))) <= (P,a) by ineq2;

          then (( - ( abs (P,a))) + ( - ( abs (P,b)))) <= (P,(a + ( - ( abs (P,b))))) by c4;

          then

           B1: ( - (( abs (P,a)) + ( abs (P,b)))) <= (P,(a + ( - ( abs (P,b))))) by RLVECT_1: 31;

          ( - ( abs (P,b))) <= (P,b) by ineq2;

          then (a + ( - ( abs (P,b)))) <= (P,(a + b)) by c4;

          hence thesis by B1, c3;

        end;

        

         B1: (a + ( abs (P,b))) <= (P,(( abs (P,a)) + ( abs (P,b)))) by c4, ineq2;

        (a + b) <= (P,(( abs (P,a)) + ( abs (P,b))))

        proof

          (a + b) <= (P,(( abs (P,b)) + a)) by c4, ineq2;

          hence thesis by B1, c3;

        end;

        hence thesis by AS1, A1, B, ineq1;

      end;

    end;

    begin

    definition

      let R be Ring;

      let a be square Element of R;

      :: REALALG2:def12

      mode SquareRoot of a -> Element of R means

      : defsqrt: (it ^2 ) = a;

      existence by O_RING_1:def 2;

    end

    notation

      let R be Ring;

      let a be square Element of R;

      synonym Sqrt of a for SquareRoot of a;

    end

    registration

      let R be non degenerated Ring;

      cluster non zero square for Element of R;

      existence

      proof

        take ( 1. R);

        thus thesis;

      end;

    end

    theorem :: REALALG2:80

    

     sq1: for R be ordered domRing, O be Ordering of R, a,b be non O -negative Element of R holds a <= (O,b) iff (a ^2 ) <= (O,(b ^2 ))

    proof

      let R be ordered domRing, P be Ordering of R, a,b be non P -negative Element of R;

      the carrier of R = (P \/ ( - P)) by REALALG1:def 8;

      then

       A: a is P -ordered & b is P -ordered;

      then

       AS: ( 0. R) <= (P,a) & ( 0. R) <= (P,b) by x1a;

      per cases ;

        suppose

         K: a = ( 0. R);

        ( SQ R) c= P & (b ^2 ) in ( SQ R) by REALALG1:def 14;

        hence thesis by A, x1a, K;

      end;

        suppose

         K: a <> ( 0. R);

        hereby

          assume a <= (P,b);

          then (a * a) <= (P,(b * a)) & (a * b) <= (P,(b * b)) by AS, c5;

          hence (a ^2 ) <= (P,(b ^2 )) by c3;

        end;

        

         C: (P * ( - P)) c= ( - P) & (P + P) c= P by v2, REALALG1:def 14;

        

         B: (a + b) in (P + P) by AS;

        

         D: the carrier of R = (P \/ ( - P)) by REALALG1:def 8;

        assume (a ^2 ) <= (P,(b ^2 ));

        then

         A: ((b + a) * (b - a)) in P by P4a;

        per cases by D, XBOOLE_0:def 3;

          suppose (b - a) in ( - P);

          then ((b + a) * (b - a)) in (P * ( - P)) by B, C;

          then ((b + a) * (b - a)) in (P /\ ( - P)) by A, C;

          then ((b + a) * (b - a)) in {( 0. R)} by REALALG1:def 7;

          then

           D: ((b + a) * (b - a)) = ( 0. R) by TARSKI:def 1;

          per cases by D, VECTSP_2:def 1;

            suppose (b + a) = ( 0. R);

            then a = ( - b) by RLVECT_1: 6;

            then a in ( - P) by AS;

            then a in (P /\ ( - P)) by AS;

            then a in {( 0. R)} by REALALG1:def 7;

            hence a <= (P,b) by K, TARSKI:def 1;

          end;

            suppose (b - a) = ( 0. R);

            hence a <= (P,b) by REALALG1: 25;

          end;

        end;

          suppose (b - a) in P;

          hence a <= (P,b);

        end;

      end;

    end;

    

     sq0: for R be preordered domRing, P be Preordering of R, a be square Element of R holds for b1,b2 be Sqrt of a st ( 0. R) <= (P,b1) & ( 0. R) <= (P,b2) holds b1 = b2

    proof

      let R be preordered domRing, P be Preordering of R, a be square Element of R;

      let b1,b2 be Sqrt of a;

      assume

       AS: ( 0. R) <= (P,b1) & ( 0. R) <= (P,b2);

      per cases ;

        suppose

         A: b1 = ( 0. R);

        

        then ( 0. R) = (b1 ^2 )

        .= a by defsqrt

        .= (b2 ^2 ) by defsqrt

        .= (b2 * b2);

        hence thesis by A, VECTSP_2:def 1;

      end;

        suppose b1 <> ( 0. R);

        then

         A: ( - b1) < (P,( - ( 0. R))) by AS, c10a;

        (b1 ^2 ) = a by defsqrt

        .= (b2 ^2 ) by defsqrt;

        then b1 = b2 or b1 = ( - b2) by sq00;

        hence thesis by A, AS, c2;

      end;

    end;

    theorem :: REALALG2:81

    for R be ordered domRing, O be Ordering of R, a,b be non O -negative Element of R holds a < (O,b) iff (a ^2 ) < (O,(b ^2 ))

    proof

      let R be ordered domRing, P be Ordering of R, a,b be non P -negative Element of R;

      the carrier of R = (P \/ ( - P)) by REALALG1:def 8;

      then a is P -ordered & b is P -ordered;

      then

       AS: ( 0. R) <= (P,a) & ( 0. R) <= (P,b) by x1a;

      hereby

        assume

         K: a < (P,b);

        a is Sqrt of (a ^2 ) & b is Sqrt of (b ^2 ) by defsqrt;

        hence (a ^2 ) < (P,(b ^2 )) by K, AS, sq1, sq0;

      end;

      thus thesis by sq1;

    end;

    theorem :: REALALG2:82

    for R be preordered domRing, P be Preordering of R, a be P -ordered Element of R holds (( abs (P,a)) ^2 ) = (a ^2 )

    proof

      let R be preordered domRing, P be Preordering of R, a be P -ordered Element of R;

      a in (P \/ ( - P)) by defppp;

      per cases by XBOOLE_0:def 3;

        suppose a in P;

        then ( 0. R) <= (P,a);

        hence thesis by av2;

      end;

        suppose a in ( - P);

        then ( - a) in ( - ( - P));

        then a <= (P,( 0. R));

        

        hence (( abs (P,a)) ^2 ) = (( - a) ^2 ) by av3

        .= (a ^2 ) by VECTSP_1: 10;

      end;

    end;

    theorem :: REALALG2:83

    

     sq5: for R be preordered Ring, P be Preordering of R, a be Element of R st a in (( - P) \ {( 0. R)}) holds a is non square

    proof

      let R be preordered Ring, P be Preordering of R, a be Element of R;

      assume a in (( - P) \ {( 0. R)});

      then

       A: a in ( - P) & not a in {( 0. R)} by XBOOLE_0:def 5;

      

       B: ( SQ R) c= P & (P /\ ( - P)) = {( 0. R)} by REALALG1:def 14;

      assume a is square;

      then a in ( SQ R);

      hence contradiction by A, B;

    end;

    theorem :: REALALG2:84

    for R be preordered Ring, P be Preordering of R holds (( - P) /\ ( SQ R)) = {( 0. R)}

    proof

      let R be preordered Ring, P be Preordering of R;

      ( 0. R) in P by REALALG1: 25;

      then

       C: ( - ( 0. R)) in ( - P);

       A:

      now

        let o be object;

        assume o in {( 0. R)};

        then o = ( 0. R) by TARSKI:def 1;

        then o in ( - P) & o in ( SQ R) by C;

        hence o in (( - P) /\ ( SQ R));

      end;

      now

        let o be object;

        assume o in (( - P) /\ ( SQ R));

        then

         H0: o in ( - P) & o in ( SQ R) by XBOOLE_0:def 4;

        then

        consider a be Element of R such that

         H1: o = a & a is square;

         not (a in (( - P) \ {( 0. R)})) by H1, sq5;

        hence o in {( 0. R)} by H0, H1, XBOOLE_0:def 5;

      end;

      hence thesis by A, TARSKI: 2;

    end;

    theorem :: REALALG2:85

    for R be preordered domRing, P be Preordering of R, a be square Element of R holds for b1,b2 be Sqrt of a st ( 0. R) <= (P,b1) & ( 0. R) <= (P,b2) holds b1 = b2 by sq0;

    

     lemsqrtex: for R be ordered domRing, O be Ordering of R, a be square Element of R holds ex b be Sqrt of a st b is non O -negative

    proof

      let R be ordered domRing, O be Ordering of R, a be square Element of R;

      consider b be Element of R such that

       H: (b ^2 ) = a by O_RING_1:def 2;

      reconsider b as Sqrt of a by H, defsqrt;

      

       A: (O \/ ( - O)) = the carrier of R by REALALG1:def 8;

      per cases ;

        suppose

         C: b = ( 0. R);

        take b;

        thus thesis by C;

      end;

        suppose

         X: b <> ( 0. R);

        per cases by A, XBOOLE_0:def 3;

          suppose b in O;

          then ( 0. R) <= (O,b);

          then

           B: ( 0. R) < (O,b) by X;

          take b;

          thus thesis by B, x1;

        end;

          suppose b in ( - O);

          then ( - b) in ( - ( - O));

          then ( 0. R) <= (O,( - b));

          then

           B: ( 0. R) < (O,( - b)) by X;

          set c = ( - b);

          (c ^2 ) = (b ^2 ) by VECTSP_1: 10;

          then

          reconsider c as Sqrt of a by defsqrt;

          take c;

          thus thesis by B, x1;

        end;

      end;

    end;

    registration

      let R be preordered Ring;

      let P be Preordering of R;

      cluster P -negative -> non square for Element of R;

      coherence by sq5;

      cluster non P -positive square -> zero for Element of R;

      coherence

      proof

        let a be Element of R;

        assume

         AS: a is non P -positive square;

        then not a in P or a in {( 0. R)} by XBOOLE_0:def 5;

        per cases by TARSKI:def 1;

          suppose

           B: not a in P;

          

           C: a in ( SQ R) by AS;

          

           D: ( SQ R) c= ( QS R) by REALALG1: 18;

          ( QS R) c= P by REALALG1: 24;

          hence thesis by B, C, D;

        end;

          suppose a = ( 0. R);

          hence thesis;

        end;

      end;

    end

    registration

      let R be ordered domRing;

      let O be Ordering of R;

      let a be square Element of R;

      cluster non O -negative for Sqrt of a;

      existence by lemsqrtex;

    end

    registration

      let R be ordered domRing;

      let O be Ordering of R;

      let a be non zero square Element of R;

      cluster O -positive for Sqrt of a;

      existence

      proof

        consider b be Sqrt of a such that

         A: b is non O -negative by lemsqrtex;

         B:

        now

          assume b = ( 0. R);

          then ( 0. R) = (b ^2 );

          hence contradiction by defsqrt;

        end;

        take b;

         not b < (O,( 0. R)) by A, x2;

        then ( 0. R) < (O,b) by B, avb4;

        hence thesis by x1;

      end;

      cluster O -negative for Sqrt of a;

      existence

      proof

        consider b be Sqrt of a such that

         A: b is non O -negative by lemsqrtex;

         B:

        now

          assume b = ( 0. R);

          then ( 0. R) = (b ^2 );

          hence contradiction by defsqrt;

        end;

        take ( - b);

        

         C: (( - b) ^2 ) = (b ^2 ) by VECTSP_1: 10

        .= a by defsqrt;

         not b < (O,( 0. R)) by A, x2;

        then ( 0. R) < (O,b) by B, avb4;

        then ( - b) < (O,( - ( 0. R))) by c10a;

        hence thesis by C, defsqrt, x2;

      end;

    end

    definition

      let R be ordered domRing;

      let O be Ordering of R;

      let a be square Element of R;

      :: REALALG2:def13

      func sqrt (O,a) -> non O -negative Sqrt of a means

      : defq: (it ^2 ) = a;

      existence

      proof

        consider b be Sqrt of a such that

         A: b is non O -negative by lemsqrtex;

        reconsider b as non O -negative Sqrt of a by A;

        take b;

        thus thesis by defsqrt;

      end;

      uniqueness

      proof

        now

          let b1,b2 be non O -negative Element of R;

          assume

           A: (b1 ^2 ) = a & (b2 ^2 ) = a;

          then

           A1: b1 is Sqrt of a & b2 is Sqrt of a by defsqrt;

          per cases ;

            suppose b1 = ( 0. R);

            hence b1 = b2 by A, VECTSP_2:def 1;

          end;

            suppose

             X: b1 <> ( 0. R);

             C:

            now

              assume not (( 0. R) <= (O,b1));

              then b1 <= (O,( 0. R)) & (b1 < (O,( 0. R)) or b1 = ( 0. R)) by avb4;

              hence contradiction by X, x2;

            end;

            now

              assume not (( 0. R) <= (O,b2));

              then b2 <= (O,( 0. R)) & (b2 < (O,( 0. R)) or b2 = ( 0. R)) by avb4;

              hence contradiction by x2, X, A, VECTSP_2:def 1;

            end;

            hence b1 = b2 by A1, C, sq0;

          end;

        end;

        hence thesis;

      end;

    end

    theorem :: REALALG2:86

    for R be ordered domRing, O be Ordering of R, a be square Element of R, b be Element of R holds b is Sqrt of a iff (b = ( sqrt (O,a)) or b = ( - ( sqrt (O,a))))

    proof

      let R be ordered domRing, O be Ordering of R;

      let a be square Element of R, b be Element of R;

      hereby

        assume b is Sqrt of a;

        

        then (b ^2 ) = a by defsqrt

        .= (( sqrt (O,a)) ^2 ) by defq;

        hence b = ( sqrt (O,a)) or b = ( - ( sqrt (O,a))) by sq00;

      end;

      assume b = ( sqrt (O,a)) or b = ( - ( sqrt (O,a)));

      per cases ;

        suppose b = ( sqrt (O,a));

        hence b is Sqrt of a;

      end;

        suppose

         B: b = ( - ( sqrt (O,a)));

        (( - ( sqrt (O,a))) ^2 ) = (( sqrt (O,a)) ^2 ) by VECTSP_1: 10;

        hence b is Sqrt of a by B, defsqrt;

      end;

    end;

    registration

      let R be ordered domRing;

      let O be Ordering of R;

      let a be non zero square Element of R;

      cluster ( sqrt (O,a)) -> non zero;

      coherence

      proof

        a = (( sqrt (O,a)) ^2 ) by defq;

        hence thesis;

      end;

    end