let p, q be ExtReal; :: thesis: ( p <= q implies [.p,q.] = [.p,q.] \/ [.q,p.] )
assume A1: p <= q ; :: thesis: [.p,q.] = [.p,q.] \/ [.q,p.]
then A2: [.q,p.] c= {p} by Th85;
p in [.p,q.] by A1, Th1;
then {p} c= [.p,q.] by ZFMISC_1:31;
hence [.p,q.] = [.p,q.] \/ [.q,p.] by A2, XBOOLE_1:1, XBOOLE_1:12; :: thesis: verum