let A be closed-interval Subset of REAL ; :: thesis: not A is empty
consider a, b being Real such that
A1: ( a <= b & A = [.a,b.] ) by Def1;
[.a,b.] = { x where x is Real : ( a <= x & x <= b ) } by RCOMP_1:def 1;
then a in A by A1;
hence not A is empty ; :: thesis: verum