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₁ being ExtReal st b₁ = m - (Depth phi) holds
not b₁ is negative ; :: thesis: verum