let p, q be ExtReal; :: thesis: ( p <= q implies ].q,p.[ = {} )
assume p <= q ; :: thesis: ].q,p.[ = {}
then [.q,p.[ = {} by Th27;
hence ].q,p.[ = {} by Th22, XBOOLE_1:3; :: thesis: verum