let p, q be ExtReal; :: thesis: ].p,q.[ c= [.p,q.]
A1: ].p,q.[ c= [.p,q.[ by Th22;
[.p,q.[ c= [.p,q.] by Th24;
hence ].p,q.[ c= [.p,q.] by A1; :: thesis: verum