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))
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
A1: 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;
A2: x in LSeg (S-max (L~ f)),(SE-corner (L~ f)) by A1, XBOOLE_0:def 4;
reconsider p = x as Point of (TOP-REAL 2) by A1;
A3: p in LSeg (NW-corner (L~ f)),(N-min (L~ f)) by A1, XBOOLE_0:def 4;
( (NW-corner (L~ f)) `2 = N-bound (L~ f) & (N-min (L~ f)) `2 = N-bound (L~ f) ) by EUCLID:56;
then ( N-bound (L~ f) <= p `2 & p `2 <= N-bound (L~ f) ) by A3, TOPREAL1:10;
then A4: p `2 = N-bound (L~ f) by XXREAL_0:1;
( (SE-corner (L~ f)) `2 = S-bound (L~ f) & (S-max (L~ f)) `2 = S-bound (L~ f) ) by EUCLID:56;
then ( S-bound (L~ f) <= p `2 & p `2 <= S-bound (L~ f) ) by A2, TOPREAL1:10;
hence contradiction by A4, TOPREAL5:22; :: thesis: verum