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

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