let A be closed-interval Subset of REAL ; not A is empty
consider a, b being Real such that
A1:
a <= b
and
A2:
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, A2;
hence
not A is empty
; verum