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

let x be set ; :: thesis: ( x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r2' & p `2 >= r1' ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r2' ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r1' ) or ( p `1 = r2 & p `2 <= r2' & p `2 >= r1' ) ) } implies x in ({ p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r1' <= p `2 & p `2 <= r2' ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r2' & r1 <= p `1 & p `1 <= r2 ) } ) \/ ({ p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r1' <= p `2 & p `2 <= r2' ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r1' & r1 <= p `1 & p `1 <= r2 ) } ) )
assume x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r2' & p `2 >= r1' ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r2' ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r1' ) or ( p `1 = r2 & p `2 <= r2' & p `2 >= r1' ) ) } ; :: thesis: x in ({ p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r1' <= p `2 & p `2 <= r2' ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r2' & r1 <= p `1 & p `1 <= r2 ) } ) \/ ({ p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r1' <= p `2 & p `2 <= r2' ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r1' & r1 <= p `1 & p `1 <= r2 ) } )
then consider p being Point of (TOP-REAL 2) such that
A4: x = p and
A5: ( ( p `1 = r1 & p `2 <= r2' & p `2 >= r1' ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r2' ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r1' ) or ( p `1 = r2 & p `2 <= r2' & p `2 >= r1' ) ) ;
( x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r1' <= p `2 & p `2 <= r2' ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `2 = r2' & r1 <= p `1 & p `1 <= r2 ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r1' <= p `2 & p `2 <= r2' ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `2 = r1' & r1 <= p `1 & p `1 <= r2 ) } ) by A4, A5;
then ( x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r1' <= p `2 & p `2 <= r2' ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r2' & r1 <= p `1 & p `1 <= r2 ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r1' <= p `2 & p `2 <= r2' ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r1' & 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 & r1' <= p `2 & p `2 <= r2' ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r2' & r1 <= p `1 & p `1 <= r2 ) } ) \/ ({ p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r1' <= p `2 & p `2 <= r2' ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r1' & r1 <= p `1 & p `1 <= r2 ) } ) by XBOOLE_0:def 3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ({ p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r1' <= p `2 & p `2 <= r2' ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r2' & r1 <= p `1 & p `1 <= r2 ) } ) \/ ({ p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r1' <= p `2 & p `2 <= r2' ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r1' & r1 <= p `1 & p `1 <= r2 ) } ) or x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r2' & p `2 >= r1' ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r2' ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r1' ) or ( p `1 = r2 & p `2 <= r2' & p `2 >= r1' ) ) } )
assume x in ({ p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r1' <= p `2 & p `2 <= r2' ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r2' & r1 <= p `1 & p `1 <= r2 ) } ) \/ ({ p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r1' <= p `2 & p `2 <= r2' ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r1' & r1 <= p `1 & p `1 <= r2 ) } ) ; :: thesis: x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r2' & p `2 >= r1' ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r2' ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r1' ) or ( p `1 = r2 & p `2 <= r2' & p `2 >= r1' ) ) }
then A6: ( x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r1' <= p `2 & p `2 <= r2' ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r2' & r1 <= p `1 & p `1 <= r2 ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r1' <= p `2 & p `2 <= r2' ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r1' & 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 & r1' <= p `2 & p `2 <= r2' ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `2 = r2' & r1 <= p `1 & p `1 <= r2 ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r1' <= p `2 & p `2 <= r2' ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `2 = r1' & r1 <= p `1 & p `1 <= r2 ) } ) by A6, XBOOLE_0:def 3;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

end;

end;

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