consider D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) such that
A1: f = SpStSeq D by Def2;
A2: W-bound D < E-bound D by Th33;
A3: S-bound D < N-bound D by Th34;
L~ f = [.(W-bound D),(E-bound D),(S-bound D),(N-bound D).] by A1, Th44;
hence L~ f is Jordan by A2, A3, Th95; :: thesis: verum