W-bound (L~ f) <> E-bound (L~ f) by TOPREAL5:23;
hence not L~ f is vertical by SPRECT_1:17; :: thesis: not L~ f is horizontal
S-bound (L~ f) <> N-bound (L~ f) by TOPREAL5:22;
hence not L~ f is horizontal by SPRECT_1:18; :: thesis: verum