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))) = {}
A1: ( (NE-corner (L~ f)) `1 = E-bound (L~ f) & (E-max (L~ f)) `1 = E-bound (L~ f) ) by EUCLID:56;
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
A2: 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;
reconsider p = x as Point of (TOP-REAL 2) by A2;
p in LSeg (NE-corner (L~ f)),(E-max (L~ f)) by A2, XBOOLE_0:def 4;
then ( E-bound (L~ f) <= p `1 & p `1 <= E-bound (L~ f) ) by A1, TOPREAL1:9;
then A3: p `1 = E-bound (L~ f) by XXREAL_0:1;
A4: (NW-corner (L~ f)) `1 <= (N-min (L~ f)) `1 by PSCOMP_1:97;
(N-max (L~ f)) `1 <= (NE-corner (L~ f)) `1 by PSCOMP_1:97;
then A5: (N-min (L~ f)) `1 < (NE-corner (L~ f)) `1 by Th55, XXREAL_0:2;
x in LSeg (N-min (L~ f)),(NW-corner (L~ f)) by A2, XBOOLE_0:def 4;
then p `1 <= (N-min (L~ f)) `1 by A4, TOPREAL1:9;
hence contradiction by A3, A5, EUCLID:56; :: thesis: verum