let A be non empty closed_interval Subset of REAL; :: thesis: for a1, a2, b1, b2 being Real st A = [.a1,b1.] & A = [.a2,b2.] holds
( a1 = a2 & b1 = b2 )
let a1, a2, b1, b2 be Real; :: thesis: ( A = [.a1,b1.] & A = [.a2,b2.] implies ( a1 = a2 & b1 = b2 ) )
assume that
A1: A = [.a1,b1.] and
A2: A = [.a2,b2.] ; :: thesis: ( a1 = a2 & b1 = b2 )
a1 <= b1 by A1, XXREAL_1:29;
hence ( a1 = a2 & b1 = b2 ) by A1, A2, XXREAL_1:66; :: thesis: verum