let R be Ring; :: thesis: for p being Polynomial of R
for r being Real st r in REAL+ holds
p <> r
let p be Polynomial of R; :: thesis: for r being Real st r in REAL+ holds
p <> r
let x be Real; :: thesis: ( x in REAL+ implies p <> x )
assume A1: x in REAL+ ; :: thesis: p <> x
A2: dom p = NAT by FUNCT_2:def 1;
then A3: ( [0,(p . 0)] in p & [1,(p . 1)] in p ) by FUNCT_1:def 2;

now :: thesis: not p = x

assume A4: p = x ; :: thesis: contradiction

per cases ( x is Rational or not x is Rational ) ;

suppose x is Rational ; :: thesis: contradiction

hence contradiction by A4, Th20; :: thesis: verum

end;

suppose x is not Rational ; :: thesis: contradiction

then not x in RAT ;
then ( not x in RAT+ \/ [:{0},RAT+:] or x in {[0,0]} ) by NUMBERS:def 3, XBOOLE_0:def 5;

per cases then ( x in {[0,0]} or ( not x in RAT+ & not x in [:{0},RAT+:] ) ) by XBOOLE_0:def 3;

suppose A5: x in {[0,0]} ; :: thesis: contradiction

[0,0] = {{0},{0,0}} by TARSKI:def 5;
hence contradiction by A2, A4, A5; :: thesis: verum

end;

suppose ( not x in RAT+ & not x in [:{0},RAT+:] ) ; :: thesis: contradiction

then x in DEDEKIND_CUTS by A1, ARYTM_2:def 2, XBOOLE_0:def 3;
then ( x in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } & not x in {RAT+} ) by ARYTM_2:def 1, XBOOLE_0:def 5;
then consider A being Subset of RAT+ such that
A6: ( x = A & ( for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) ) ) ;
consider u being Element of A such that
A7: u = [0,(p . 0)] by A3, A4, A6;
u in A by A4, A6;
then reconsider u = u as Element of RAT+ ;

per cases ( u in omega or u in { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } \ { [k,1] where k is Element of omega : verum } ) by XBOOLE_0:def 3;

suppose u in omega ; :: thesis: contradiction

then reconsider n = u as Element of omega ;
n = {1,1} by A7;
hence contradiction by A7; :: thesis: verum

end;

suppose u in { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } \ { [k,1] where k is Element of omega : verum } ; :: thesis: contradiction

then A8: ( u in { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } & not u in { [k,1] where k is Element of omega : verum } ) by XBOOLE_0:def 5;
then consider i, j being Element of omega such that
A9: ( u = [i,j] & i,j are_coprime & j <> {} ) ;
i = 0 by A7, A9, XTUPLE_0:1;
then j = 1 by A9, ARYTM_3:3;
hence contradiction by A8, A9; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

hence p <> x ; :: thesis: verum