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