let f be 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:52;
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 object 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:3;
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:38;
(N-max (L~ f)) `1 <= (NE-corner (L~ f)) `1 by PSCOMP_1:38;
then A5: (N-min (L~ f)) `1 < (NE-corner (L~ f)) `1 by Th51, 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:3;
hence contradiction by A3, A5, EUCLID:52; :: thesis: verum