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 ) )

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