let f be constant standard special_circular_sequence; :: thesis: LSeg ((S-max (L~ f)),(SE-corner (L~ f))) misses LSeg ((NW-corner (L~ f)),(N-min (L~ f)))
A1: ( (NW-corner (L~ f)) `2 = N-bound (L~ f) & (N-min (L~ f)) `2 = N-bound (L~ f) ) by EUCLID:52;
assume LSeg ((S-max (L~ f)),(SE-corner (L~ f))) meets LSeg ((NW-corner (L~ f)),(N-min (L~ f))) ; :: thesis: contradiction
then (LSeg ((S-max (L~ f)),(SE-corner (L~ f)))) /\ (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) <> {} ;
then consider x being object such that
A2: x in (LSeg ((S-max (L~ f)),(SE-corner (L~ f)))) /\ (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) by XBOOLE_0:def 1;
reconsider p = x as Point of (TOP-REAL 2) by A2;
p in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by A2, XBOOLE_0:def 4;
then ( N-bound (L~ f) <= p `2 & p `2 <= N-bound (L~ f) ) by A1, TOPREAL1:4;
then A3: p `2 = N-bound (L~ f) by XXREAL_0:1;
A4: ( (SE-corner (L~ f)) `2 = S-bound (L~ f) & (S-max (L~ f)) `2 = S-bound (L~ f) ) by EUCLID:52;
x in LSeg ((S-max (L~ f)),(SE-corner (L~ f))) by A2, XBOOLE_0:def 4;
then p `2 <= S-bound (L~ f) by A4, TOPREAL1:4;
hence contradiction by A3, TOPREAL5:16; :: thesis: verum