let f be rectangular special_circular_sequence; :: thesis: for p being Point of (TOP-REAL 2) st ( W-bound (L~ f) > p `1 or p `1 > E-bound (L~ f) or S-bound (L~ f) > p `2 or p `2 > N-bound (L~ f) ) holds
p in LeftComp f
let p be Point of (TOP-REAL 2); :: thesis: ( ( W-bound (L~ f) > p `1 or p `1 > E-bound (L~ f) or S-bound (L~ f) > p `2 or p `2 > N-bound (L~ f) ) implies p in LeftComp f )
LeftComp f = { q where q is Point of (TOP-REAL 2) : ( not W-bound (L~ f) <= q `1 or not q `1 <= E-bound (L~ f) or not S-bound (L~ f) <= q `2 or not q `2 <= N-bound (L~ f) ) } by Th37;
hence ( ( W-bound (L~ f) > p `1 or p `1 > E-bound (L~ f) or S-bound (L~ f) > p `2 or p `2 > N-bound (L~ f) ) implies p in LeftComp f ) ; :: thesis: verum