theorem Th35: :: JGRAPH_6:35

{ 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 ) ) } = { 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 ) ) }