let f be V22() standard special_circular_sequence; :: thesis: LSeg ((NW-corner (L~ f)),(N-min (L~ f))) misses LSeg ((N-max (L~ f)),(NE-corner (L~ f)))
A1: (N-min (L~ f)) `2 = (N-max (L~ f)) `2 by PSCOMP_1:37;
assume LSeg ((NW-corner (L~ f)),(N-min (L~ f))) meets LSeg ((N-max (L~ f)),(NE-corner (L~ f))) ; :: thesis: contradiction
then consider p being object such that
A2: p in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) and
A3: p in LSeg ((N-max (L~ f)),(NE-corner (L~ f))) by XBOOLE_0:3;
reconsider p = p as Point of (TOP-REAL 2) by A2;
(N-max (L~ f)) `1 <= (NE-corner (L~ f)) `1 by PSCOMP_1:38;
then A4: (N-max (L~ f)) `1 <= p `1 by A3, TOPREAL1:3;
(NW-corner (L~ f)) `1 <= (N-min (L~ f)) `1 by PSCOMP_1:38;
then p `1 <= (N-min (L~ f)) `1 by A2, TOPREAL1:3;
then A5: (N-min (L~ f)) `1 >= (N-max (L~ f)) `1 by A4, XXREAL_0:2;
(N-min (L~ f)) `1 <= (N-max (L~ f)) `1 by PSCOMP_1:38;
then (N-min (L~ f)) `1 = (N-max (L~ f)) `1 by A5, XXREAL_0:1;
hence contradiction by A1, Th52, TOPREAL3:6; :: thesis: verum