let a, b be Real; :: thesis: for A being non empty closed_interval Subset of REAL st A = [.a,b.] holds
( upper_bound A = b & lower_bound A = a )
let A be non empty closed_interval Subset of REAL; :: thesis: ( A = [.a,b.] implies ( upper_bound A = b & lower_bound A = a ) )
A1: A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
assume A = [.a,b.] ; :: thesis: ( upper_bound A = b & lower_bound A = a )
hence ( upper_bound A = b & lower_bound A = a ) by A1, INTEGRA1:5; :: thesis: verum