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 Th31;
A3: S-bound D < N-bound D by Th32;
L~ f = [.(W-bound D),(E-bound D),(S-bound D),(N-bound D).] by A1, Th42;
hence L~ f is Jordan by A2, A3, Th87; :: thesis: verum