let p, q be ext-real number ; :: thesis: ].p,q.[ c= [.p,q.]
( ].p,q.[ c= [.p,q.[ & [.p,q.[ c= [.p,q.] ) by Th22, Th24;
hence ].p,q.[ c= [.p,q.] by XBOOLE_1:1; :: thesis: verum