hereby :: thesis: ( ( for r being Element of RAT+ holds
not for s being Element of RAT+ holds
( s in x iff s < r ) ) implies ex b₁ being Element of REAL+ st b₁ = x )

given r being Element of RAT+ such that A5: for s being Element of RAT+ holds
( s in x iff s < r ) ; :: thesis: ex y being Element of REAL+ ex r being Element of RAT+ st
( y = r & ( for s being Element of RAT+ holds
( s in x iff s < r ) ) )
reconsider y = r as Element of REAL+ by Th1;
take y = y; :: thesis: ex r being Element of RAT+ st
( y = r & ( for s being Element of RAT+ holds
( s in x iff s < r ) ) )
take r = r; :: thesis: ( y = r & ( for s being Element of RAT+ holds
( s in x iff s < r ) ) )
thus y = r ; :: thesis: for s being Element of RAT+ holds
( s in x iff s < r )
thus for s being Element of RAT+ holds
( s in x iff s < r ) by A5; :: thesis: verum

end;

assume A6: for r being Element of RAT+ holds
not for s being Element of RAT+ holds
( s in x iff s < r ) ; :: thesis: ex b₁ being Element of REAL+ st b₁ = x

now :: thesis: not x in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} }

assume x in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ; :: thesis: contradiction
then consider t being Element of RAT+ such that
A7: x = { s where s is Element of RAT+ : s < t } and
t <> {} ;
for s being Element of RAT+ holds
( s in x iff s < t )

proof

let s be Element of RAT+ ; :: thesis: ( s in x iff s < t )

hereby :: thesis: ( s < t implies s in x )

assume s in x ; :: thesis: s < t
then ex r being Element of RAT+ st
( s = r & r < t ) by A7;
hence s < t ; :: thesis: verum

end;

thus ( s < t implies s in x ) by A7; :: thesis: verum

end;

hence contradiction by A6; :: thesis: verum

end;

then x in DEDEKIND_CUTS \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } by XBOOLE_0:def 5;
then reconsider y = x as Element of REAL+ by Lm4;
take y ; :: thesis: y = x
thus y = x ; :: thesis: verum