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