let p, q be ext-real number ; :: 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, XBOOLE_1:1; :: thesis: verum