set R = F_Real ;
let P be Preordering of F_Real; :: thesis: P is spanning
A: SQ F_Real c= P by REALALG1:def 14;

now :: thesis: for o being object st o in the carrier of F_Real holds
o in P \/ (- P)

let o be object ; :: thesis: ( o in the carrier of F_Real implies b₁ in P \/ (- P) )
assume o in the carrier of F_Real ; :: thesis: b₁ in P \/ (- P)
then reconsider x = o as Element of REAL ;

per cases ( 0 <= x or x <= 0 ) ;

suppose B: 0 <= x ; :: thesis: b₁ in P \/ (- P)

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 F_Real ;
hence o in P \/ (- P) by A, XBOOLE_0:def 3; :: thesis: verum

end;

suppose B: x <= 0 ; :: thesis: b₁ in P \/ (- P)

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 F_Real ;
then - (a |^ 2) in - P by A, C;
hence o in P \/ (- P) by C, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

then the carrier of F_Real = P \/ (- P) by TARSKI:def 3;
hence P is spanning ; :: thesis: verum