let a, b, c, d be real number ; :: thesis: ( a < b & c < d implies rectangle a,b,c,d is being_simple_closed_curve )
assume A1: ( a < b & 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;
A2: ( 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 Th59;
|[a,c]| `1 = a by EUCLID:56;
then A3: |[a,c]| <> |[b,d]| by A1, EUCLID:56;
|[a,c]| in (L~ f1) /\ (L~ f2) by A1, A2, Lm8, TARSKI:def 2;
then |[a,c]| in L~ f1 by XBOOLE_0:def 4;
then A4: |[a,c]| in rectangle a,b,c,d by A1, A2, Lm8, XBOOLE_0:def 3;
|[b,d]| in (L~ f1) /\ (L~ f2) by A1, A2, Lm8, 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, Lm8, XBOOLE_0:def 3;
hence rectangle a,b,c,d is being_simple_closed_curve by A1, A2, A3, A4, Lm8, TOPREAL2:6; :: thesis: verum