scheme :: XXREAL_1:sch 1
Conti{ P₁[ object ], P₂[ object ] } :

ex s being ExtReal st
( ( for r being ExtReal st P₁[r] holds
r <= s ) & ( for r being ExtReal st P₂[r] holds
s <= r ) )

provided

A1: for r, s being ExtReal st P₁[r] & P₂[s] holds
r <= s