let IT1, IT2 be Element of REAL+ ; :: thesis: ( ( ex r being Element of RAT+ st
for s being Element of RAT+ holds
( s in x iff s < r ) & ex r being Element of RAT+ st
( IT1 = r & ( for s being Element of RAT+ holds
( s in x iff s < r ) ) ) & ex r being Element of RAT+ st
( IT2 = r & ( for s being Element of RAT+ holds
( s in x iff s < r ) ) ) implies IT1 = IT2 ) & ( ( for r being Element of RAT+ holds
not for s being Element of RAT+ holds
( s in x iff s < r ) ) & IT1 = x & IT2 = x implies IT1 = IT2 ) )
hereby :: thesis: ( ( for r being Element of RAT+ holds
not for s being Element of RAT+ holds
( s in x iff s < r ) ) & IT1 = x & IT2 = x implies IT1 = IT2 )
assume ex r being Element of RAT+ st
for s being Element of RAT+ holds
( s in x iff s < r ) ; :: thesis: ( ex r1 being Element of RAT+ st
( IT1 = r1 & ( for s being Element of RAT+ holds
( s in x iff s < r1 ) ) ) & ex r2 being Element of RAT+ st
( IT2 = r2 & ( for s being Element of RAT+ holds
( s in x iff s < r2 ) ) ) implies IT1 = IT2 )
given r1 being Element of RAT+ such that A1: IT1 = r1 and
A2: for s being Element of RAT+ holds
( s in x iff s < r1 ) ; :: thesis: ( ex r2 being Element of RAT+ st
( IT2 = r2 & ( for s being Element of RAT+ holds
( s in x iff s < r2 ) ) ) implies IT1 = IT2 )
given r2 being Element of RAT+ such that A3: IT2 = r2 and
A4: for s being Element of RAT+ holds
( s in x iff s < r2 ) ; :: thesis: IT1 = IT2
for s being Element of RAT+ holds
( s < r1 iff s < r2 ) by A2, A4;
hence IT1 = IT2 by A1, A3, Lm6; :: thesis: verum
end;
thus ( ( for r being Element of RAT+ holds
not for s being Element of RAT+ holds
( s in x iff s < r ) ) & IT1 = x & IT2 = x implies IT1 = IT2 ) ; :: thesis: verum