take <*> REAL ; :: thesis: ( <*> REAL is non-increasing & <*> REAL is non-decreasing )
thus ( <*> REAL is non-increasing & <*> REAL is non-decreasing ) ; :: thesis: verum