let a, b, c, d be Real; :: thesis: ( a < b & c < d implies rectangle (a,b,c,d) is being_simple_closed_curve )
assume that
A1: a < b and
A2: c < d ; :: thesis: rectangle (a,b,c,d) is being_simple_closed_curve
set P = rectangle (a,b,c,d);
set p1 = |[a,c]|;
set p2 = |[b,d]|;
reconsider f1 = <*|[a,c]|,|[a,d]|,|[b,d]|*> as FinSequence of (TOP-REAL 2) ;
reconsider f2 = <*|[a,c]|,|[b,c]|,|[b,d]|*> as FinSequence of (TOP-REAL 2) ;
set P1 = L~ f1;
set P2 = L~ f2;
A3: ( a < b & c < d & rectangle (a,b,c,d) = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = a & c <= p `2 & p `2 <= d ) or ( p `2 = d & a <= p `1 & p `1 <= b ) or ( p `1 = b & c <= p `2 & p `2 <= d ) or ( p `2 = c & a <= p `1 & p `1 <= b ) ) } & |[a,c]| = |[a,c]| & |[b,d]| = |[b,d]| & f1 = <*|[a,c]|,|[a,d]|,|[b,d]|*> & f2 = <*|[a,c]|,|[b,c]|,|[b,d]|*> & L~ f1 = L~ f1 & L~ f2 = L~ f2 implies ( L~ f1 is_an_arc_of |[a,c]|,|[b,d]| & L~ f2 is_an_arc_of |[a,c]|,|[b,d]| & not L~ f1 is empty & not L~ f2 is empty & rectangle (a,b,c,d) = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {|[a,c]|,|[b,d]|} ) ) by Th49;
|[a,c]| `1 = a by EUCLID:52;
then A4: |[a,c]| <> |[b,d]| by A1, EUCLID:52;
|[a,c]| in (L~ f1) /\ (L~ f2) by A1, A2, A3, Lm15, TARSKI:def 2;
then |[a,c]| in L~ f1 by XBOOLE_0:def 4;
then A5: |[a,c]| in rectangle (a,b,c,d) by A1, A2, A3, Lm15, XBOOLE_0:def 3;
|[b,d]| in (L~ f1) /\ (L~ f2) by A1, A2, A3, Lm15, TARSKI:def 2;
then |[b,d]| in L~ f1 by XBOOLE_0:def 4;
then |[b,d]| in rectangle (a,b,c,d) by A1, A2, A3, Lm15, XBOOLE_0:def 3;
hence rectangle (a,b,c,d) is being_simple_closed_curve by A1, A2, A3, A4, A5, Lm15, TOPREAL2:6; :: thesis: verum