let r be Real; :: thesis: ( not |[0,r]| in rectangle ((- 1),1,(- 3),3) or r = - 3 or r = 3 )
assume |[0,r]| in rectangle ((- 1),1,(- 3),3) ; :: thesis: ( r = - 3 or r = 3 )
then ex p being Point of (TOP-REAL 2) st
( p = |[0,r]| & ( ( p `1 = - 1 & p `2 <= 3 & p `2 >= - 3 ) or ( p `1 <= 1 & p `1 >= - 1 & p `2 = 3 ) or ( p `1 <= 1 & p `1 >= - 1 & p `2 = - 3 ) or ( p `1 = 1 & p `2 <= 3 & p `2 >= - 3 ) ) ) by Lm61;
hence ( r = - 3 or r = 3 ) by EUCLID:52; :: thesis: verum