set
D
=
Depth
phi
;
Depth
phi
<=
m
by
FOMODEL2:def 31
;
then
(
Depth
phi
)

(
Depth
phi
)
<=
m

(
Depth
phi
)
by
XREAL_1:9
;
hence
for
b
_{1}
being
ExtReal
st
b
_{1}
=
m

(
Depth
phi
)
holds
not
b
_{1}
is
negative
;
:: thesis:
verum