hereby :: thesis:

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

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:

now :: thesis:

assume x in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ; :: thesis:
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:

hereby :: thesis:

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

end;

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

end;

hence contradiction by A6; :: thesis:

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:
thus y = x ; :: thesis: