thus { q where q is Point of (TOP-REAL 2) : ( ( - 1 = q `1 & - 1 <= q `2 & q `2 <= 1 ) or ( q `1 = 1 & - 1 <= q `2 & q `2 <= 1 ) or ( - 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) or ( 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) ) } c= { p where p is Point of (TOP-REAL 2) : ( ( p `1 = - 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = 1 & - 1 <= p `1 & p `1 <= 1 ) or ( p `1 = 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = - 1 & - 1 <= p `1 & p `1 <= 1 ) ) } :: according to XBOOLE_0:def 10 :: thesis: { p where p is Point of (TOP-REAL 2) : ( ( p `1 = - 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = 1 & - 1 <= p `1 & p `1 <= 1 ) or ( p `1 = 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = - 1 & - 1 <= p `1 & p `1 <= 1 ) ) } c= { q where q is Point of (TOP-REAL 2) : ( ( - 1 = q `1 & - 1 <= q `2 & q `2 <= 1 ) or ( q `1 = 1 & - 1 <= q `2 & q `2 <= 1 ) or ( - 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) or ( 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is Point of (TOP-REAL 2) : ( ( - 1 = q `1 & - 1 <= q `2 & q `2 <= 1 ) or ( q `1 = 1 & - 1 <= q `2 & q `2 <= 1 ) or ( - 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) or ( 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) ) } or x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = - 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = 1 & - 1 <= p `1 & p `1 <= 1 ) or ( p `1 = 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = - 1 & - 1 <= p `1 & p `1 <= 1 ) ) } )
assume x in { q where q is Point of (TOP-REAL 2) : ( ( - 1 = q `1 & - 1 <= q `2 & q `2 <= 1 ) or ( q `1 = 1 & - 1 <= q `2 & q `2 <= 1 ) or ( - 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) or ( 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) ) } ; :: thesis: x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = - 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = 1 & - 1 <= p `1 & p `1 <= 1 ) or ( p `1 = 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = - 1 & - 1 <= p `1 & p `1 <= 1 ) ) }
then ex q being Point of (TOP-REAL 2) st
( x = q & ( ( - 1 = q `1 & - 1 <= q `2 & q `2 <= 1 ) or ( q `1 = 1 & - 1 <= q `2 & q `2 <= 1 ) or ( - 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) or ( 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) ) ) ;
hence x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = - 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = 1 & - 1 <= p `1 & p `1 <= 1 ) or ( p `1 = 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = - 1 & - 1 <= p `1 & p `1 <= 1 ) ) } ; :: thesis: verum

end;

thus { p where p is Point of (TOP-REAL 2) : ( ( p `1 = - 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = 1 & - 1 <= p `1 & p `1 <= 1 ) or ( p `1 = 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = - 1 & - 1 <= p `1 & p `1 <= 1 ) ) } c= { q where q is Point of (TOP-REAL 2) : ( ( - 1 = q `1 & - 1 <= q `2 & q `2 <= 1 ) or ( q `1 = 1 & - 1 <= q `2 & q `2 <= 1 ) or ( - 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) or ( 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) ) } :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = - 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = 1 & - 1 <= p `1 & p `1 <= 1 ) or ( p `1 = 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = - 1 & - 1 <= p `1 & p `1 <= 1 ) ) } or x in { q where q is Point of (TOP-REAL 2) : ( ( - 1 = q `1 & - 1 <= q `2 & q `2 <= 1 ) or ( q `1 = 1 & - 1 <= q `2 & q `2 <= 1 ) or ( - 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) or ( 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) ) } )
assume x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = - 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = 1 & - 1 <= p `1 & p `1 <= 1 ) or ( p `1 = 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = - 1 & - 1 <= p `1 & p `1 <= 1 ) ) } ; :: thesis: x in { q where q is Point of (TOP-REAL 2) : ( ( - 1 = q `1 & - 1 <= q `2 & q `2 <= 1 ) or ( q `1 = 1 & - 1 <= q `2 & q `2 <= 1 ) or ( - 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) or ( 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) ) }
then ex p being Point of (TOP-REAL 2) st
( p = x & ( ( p `1 = - 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = 1 & - 1 <= p `1 & p `1 <= 1 ) or ( p `1 = 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = - 1 & - 1 <= p `1 & p `1 <= 1 ) ) ) ;
hence x in { q where q is Point of (TOP-REAL 2) : ( ( - 1 = q `1 & - 1 <= q `2 & q `2 <= 1 ) or ( q `1 = 1 & - 1 <= q `2 & q `2 <= 1 ) or ( - 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) or ( 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) ) } ; :: thesis: verum

end;