begin
scheme
RSetEq{
P1[
set ] } :
for
X1,
X2 being
Subset of
REAL st ( for
x being
R_eal holds
(
x in X1 iff
P1[
x] ) ) & ( for
x being
R_eal holds
(
x in X2 iff
P1[
x] ) ) holds
X1 = X2
Lm1:
for A being Interval holds diameter A >= 0
Lm2:
for A, B being Interval st A c= B holds
diameter A <= diameter B