let f be non 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:56;
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))) <> {} by XBOOLE_0:def 7;
then consider x being set 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:10;
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:56;
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:10;
hence contradiction by A3, TOPREAL5:22; :: thesis: verum