let r1, r2, r19, r29 be Real; :: thesis: ( r1 <= r2 & r19 <= r29 implies [.r1,r2,r19,r29.] = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) } )
assume that
A1: r1 <= r2 and
A2: r19 <= r29 ; :: thesis: [.r1,r2,r19,r29.] = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) }
set p1 = |[r1,r19]|;
set p2 = |[r1,r29]|;
set p3 = |[r2,r29]|;
set p4 = |[r2,r19]|;
set P4 = { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ;
set P3 = { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } ;
set P2 = { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ;
set P1 = { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } ;
set P = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) } ;
A3: { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) } = ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } )

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ) c= { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) }

let x be object ; :: thesis: ( x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) } implies x in ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ) )
assume x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) } ; :: thesis: x in ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } )
then ex p being Point of (TOP-REAL 2) st
( x = p & ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) ) ;
then ( x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ) ;
then ( x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ) by XBOOLE_0:def 3;
hence x in ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ) by XBOOLE_0:def 3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ) or x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) } )
assume x in ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ) ; :: thesis: x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) }
then A4: ( x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ) by XBOOLE_0:def 3;

per cases ( x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ) by A4, XBOOLE_0:def 3;

suppose x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } ; :: thesis: x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) }

then ex p being Point of (TOP-REAL 2) st
( x = p & p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) ;
hence x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) } ; :: thesis: verum

end;

suppose x in { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ; :: thesis: x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) }

then ex p being Point of (TOP-REAL 2) st
( x = p & p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) ;
hence x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) } ; :: thesis: verum

end;

suppose x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } ; :: thesis: x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) }

then ex p being Point of (TOP-REAL 2) st
( x = p & p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) ;
hence x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) } ; :: thesis: verum

end;

suppose x in { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ; :: thesis: x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) }

then ex p being Point of (TOP-REAL 2) st
( x = p & p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) ;
hence x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) } ; :: thesis: verum

end;

end;

end;

thus [.r1,r2,r19,r29.] = ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ (LSeg (|[r1,r29]|,|[r2,r29]|))) \/ ((LSeg (|[r2,r29]|,|[r2,r19]|)) \/ (LSeg (|[r2,r19]|,|[r1,r19]|))) by A2, TOPREAL3:9
.= ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ) \/ ((LSeg (|[r2,r29]|,|[r2,r19]|)) \/ (LSeg (|[r2,r19]|,|[r1,r19]|))) by A1, TOPREAL3:10
.= ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ (LSeg (|[r2,r19]|,|[r1,r19]|))) by A2, TOPREAL3:9
.= { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) } by A1, A3, TOPREAL3:10 ; :: thesis: verum