let f be non constant standard special_circular_sequence; :: thesis: (LSeg (N-min (L~ f)),(NW-corner (L~ f))) /\ (LSeg (NE-corner (L~ f)),(E-max (L~ f))) = {}
assume (LSeg (N-min (L~ f)),(NW-corner (L~ f))) /\ (LSeg (NE-corner (L~ f)),(E-max (L~ f))) <> {} ; :: thesis: contradiction
then consider x being set such that
A1: x in (LSeg (N-min (L~ f)),(NW-corner (L~ f))) /\ (LSeg (NE-corner (L~ f)),(E-max (L~ f))) by XBOOLE_0:def 1;
A2: x in LSeg (N-min (L~ f)),(NW-corner (L~ f)) by A1, XBOOLE_0:def 4;
reconsider p = x as Point of (TOP-REAL 2) by A1;
A3: p in LSeg (NE-corner (L~ f)),(E-max (L~ f)) by A1, XBOOLE_0:def 4;
( (NE-corner (L~ f)) `1 = E-bound (L~ f) & (E-max (L~ f)) `1 = E-bound (L~ f) ) by EUCLID:56;
then ( E-bound (L~ f) <= p `1 & p `1 <= E-bound (L~ f) ) by A3, TOPREAL1:9;
then A4: p `1 = E-bound (L~ f) by XXREAL_0:1;
(NW-corner (L~ f)) `1 <= (N-min (L~ f)) `1 by PSCOMP_1:97;
then A5: p `1 <= (N-min (L~ f)) `1 by A2, TOPREAL1:9;
(N-max (L~ f)) `1 <= (NE-corner (L~ f)) `1 by PSCOMP_1:97;
then (N-min (L~ f)) `1 < (NE-corner (L~ f)) `1 by Th55, XXREAL_0:2;
hence contradiction by A4, A5, EUCLID:56; :: thesis: verum