set
X
=
[.
0
,1
.]
;
consider
R
being
strict
RelStr
such that
A1
: ( the
carrier
of
R
=
[.
0
,1
.]
&
R
is
real
)
by
Th1
;
take
R
;
:: thesis:
(
R
is
interval
&
R
is
strict
)
thus
(
R
is
interval
&
R
is
strict
)
by
A1
;
:: thesis:
verum