take REAL ; :: thesis: REAL is interval
thus REAL is interval ; :: thesis: verum