take the constant Real_Sequence ; :: thesis: the constant Real_Sequence is constant
thus the constant Real_Sequence is constant ; :: thesis: verum