let
a
,
b
be
Real
;
:: thesis:
for
t
being
BinOp
of
[.
0
,1
.]
holds
t
.
(
a
,
b
)
in
[.
0
,1
.]
let
t
be
BinOp
of
[.
0
,1
.]
;
:: thesis:
t
.
(
a
,
b
)
in
[.
0
,1
.]
per
cases
( (
a
in
[.
0
,1
.]
&
b
in
[.
0
,1
.]
) or not
a
in
[.
0
,1
.]
or not
b
in
[.
0
,1
.]
)
;
suppose
(
a
in
[.
0
,1
.]
&
b
in
[.
0
,1
.]
) ;
:: thesis:
t
.
(
a
,
b
)
in
[.
0
,1
.]
then
[
a
,
b
]
in
[:
[.
0
,1
.]
,
[.
0
,1
.]
:]
by
ZFMISC_1:87
;
hence
t
.
(
a
,
b
)
in
[.
0
,1
.]
by
FUNCT_2:5
;
:: thesis:
verum
end;
suppose
( not
a
in
[.
0
,1
.]
or not
b
in
[.
0
,1
.]
) ;
:: thesis:
t
.
(
a
,
b
)
in
[.
0
,1
.]
then
not
[
a
,
b
]
in
dom
t
by
ZFMISC_1:87
;
then
t
.
[
a
,
b
]
=
0
by
FUNCT_1:def 2
;
hence
t
.
(
a
,
b
)
in
[.
0
,1
.]
by
XXREAL_1:1
;
:: thesis:
verum
end;
end;