let a, b, c, d be Real; :: thesis: for f1, f2 being FinSequence of (TOP-REAL 2)

for p0, p1, p01, p10 being Point of (TOP-REAL 2) st a < b & c < d & p0 = |[a,c]| & p1 = |[b,d]| & p01 = |[a,d]| & p10 = |[b,c]| & f1 = <*p0,p01,p1*> & f2 = <*p0,p10,p1*> holds

( f1 is being_S-Seq & L~ f1 = (LSeg (p0,p01)) \/ (LSeg (p01,p1)) & f2 is being_S-Seq & L~ f2 = (LSeg (p0,p10)) \/ (LSeg (p10,p1)) & rectangle (a,b,c,d) = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {p0,p1} & f1 /. 1 = p0 & f1 /. (len f1) = p1 & f2 /. 1 = p0 & f2 /. (len f2) = p1 )

let f1, f2 be FinSequence of (TOP-REAL 2); :: thesis: for p0, p1, p01, p10 being Point of (TOP-REAL 2) st a < b & c < d & p0 = |[a,c]| & p1 = |[b,d]| & p01 = |[a,d]| & p10 = |[b,c]| & f1 = <*p0,p01,p1*> & f2 = <*p0,p10,p1*> holds

( f1 is being_S-Seq & L~ f1 = (LSeg (p0,p01)) \/ (LSeg (p01,p1)) & f2 is being_S-Seq & L~ f2 = (LSeg (p0,p10)) \/ (LSeg (p10,p1)) & rectangle (a,b,c,d) = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {p0,p1} & f1 /. 1 = p0 & f1 /. (len f1) = p1 & f2 /. 1 = p0 & f2 /. (len f2) = p1 )

let p0, p1, p01, p10 be Point of (TOP-REAL 2); :: thesis: ( a < b & c < d & p0 = |[a,c]| & p1 = |[b,d]| & p01 = |[a,d]| & p10 = |[b,c]| & f1 = <*p0,p01,p1*> & f2 = <*p0,p10,p1*> implies ( f1 is being_S-Seq & L~ f1 = (LSeg (p0,p01)) \/ (LSeg (p01,p1)) & f2 is being_S-Seq & L~ f2 = (LSeg (p0,p10)) \/ (LSeg (p10,p1)) & rectangle (a,b,c,d) = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {p0,p1} & f1 /. 1 = p0 & f1 /. (len f1) = p1 & f2 /. 1 = p0 & f2 /. (len f2) = p1 ) )

assume that

A1: a < b and

A2: c < d and

A3: p0 = |[a,c]| and

A4: p1 = |[b,d]| and

A5: p01 = |[a,d]| and

A6: p10 = |[b,c]| and

A7: f1 = <*p0,p01,p1*> and

A8: f2 = <*p0,p10,p1*> ; :: thesis: ( f1 is being_S-Seq & L~ f1 = (LSeg (p0,p01)) \/ (LSeg (p01,p1)) & f2 is being_S-Seq & L~ f2 = (LSeg (p0,p10)) \/ (LSeg (p10,p1)) & rectangle (a,b,c,d) = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {p0,p1} & f1 /. 1 = p0 & f1 /. (len f1) = p1 & f2 /. 1 = p0 & f2 /. (len f2) = p1 )

set P = rectangle (a,b,c,d);

set L1 = { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } ;

set L2 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) } ;

set L3 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) } ;

set L4 = { p where p is Point of (TOP-REAL 2) : ( p `1 = b & p `2 <= d & p `2 >= c ) } ;

A9: p1 `1 = b by A4, EUCLID:52;

A10: p1 `2 = d by A4, EUCLID:52;

A11: p10 `1 = b by A6, EUCLID:52;

A12: p10 `2 = c by A6, EUCLID:52;

A13: p0 `1 = a by A3, EUCLID:52;

A14: p0 `2 = c by A3, EUCLID:52;

A15: len f1 = 1 + 2 by A7, FINSEQ_1:45;

A16: f1 /. 1 = p0 by A7, FINSEQ_4:18;

A17: f1 /. 2 = p01 by A7, FINSEQ_4:18;

A18: f1 /. 3 = p1 by A7, FINSEQ_4:18;

thus f1 is being_S-Seq :: thesis: ( L~ f1 = (LSeg (p0,p01)) \/ (LSeg (p01,p1)) & f2 is being_S-Seq & L~ f2 = (LSeg (p0,p10)) \/ (LSeg (p10,p1)) & rectangle (a,b,c,d) = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {p0,p1} & f1 /. 1 = p0 & f1 /. (len f1) = p1 & f2 /. 1 = p0 & f2 /. (len f2) = p1 )

A41: 1 + 1 <= len f1 by A15;

LSeg (p0,p01) = LSeg (f1,1) by A15, A16, A17, A40, TOPREAL1:def 3;

then A42: LSeg (p0,p01) in { (LSeg (f1,i)) where i is Nat : ( 1 <= i & i + 1 <= len f1 ) } by A41;

LSeg (p01,p1) = LSeg (f1,2) by A15, A17, A18, TOPREAL1:def 3;

then LSeg (p01,p1) in { (LSeg (f1,i)) where i is Nat : ( 1 <= i & i + 1 <= len f1 ) } by A15;

then A43: {(LSeg (p0,p01)),(LSeg (p01,p1))} c= { (LSeg (f1,i)) where i is Nat : ( 1 <= i & i + 1 <= len f1 ) } by A42, ZFMISC_1:32;

{ (LSeg (f1,i)) where i is Nat : ( 1 <= i & i + 1 <= len f1 ) } c= {(LSeg (p0,p01)),(LSeg (p01,p1))}

hence A47: L~ f1 = (LSeg (p0,p01)) \/ (LSeg (p01,p1)) by ZFMISC_1:75; :: thesis: ( f2 is being_S-Seq & L~ f2 = (LSeg (p0,p10)) \/ (LSeg (p10,p1)) & rectangle (a,b,c,d) = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {p0,p1} & f1 /. 1 = p0 & f1 /. (len f1) = p1 & f2 /. 1 = p0 & f2 /. (len f2) = p1 )

then A48: L~ f1 = { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } \/ (LSeg (p01,p1)) by A2, A3, A5, Th30

.= { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) } by A1, A4, A5, Th30 ;

A49: len f2 = 1 + 2 by A8, FINSEQ_1:45;

A50: f2 /. 1 = p0 by A8, FINSEQ_4:18;

A51: f2 /. 2 = p10 by A8, FINSEQ_4:18;

A52: f2 /. 3 = p1 by A8, FINSEQ_4:18;

thus f2 is being_S-Seq :: thesis: ( L~ f2 = (LSeg (p0,p10)) \/ (LSeg (p10,p1)) & rectangle (a,b,c,d) = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {p0,p1} & f1 /. 1 = p0 & f1 /. (len f1) = p1 & f2 /. 1 = p0 & f2 /. (len f2) = p1 )

A74: 1 + 1 <= len f2 by A49;

LSeg (p0,p10) = LSeg (f2,1) by A49, A50, A51, A73, TOPREAL1:def 3;

then A75: LSeg (p0,p10) in { (LSeg (f2,i)) where i is Nat : ( 1 <= i & i + 1 <= len f2 ) } by A74;

LSeg (p10,p1) = LSeg (f2,2) by A49, A51, A52, TOPREAL1:def 3;

then LSeg (p10,p1) in { (LSeg (f2,i)) where i is Nat : ( 1 <= i & i + 1 <= len f2 ) } by A49;

then A76: {(LSeg (p0,p10)),(LSeg (p10,p1))} c= { (LSeg (f2,i)) where i is Nat : ( 1 <= i & i + 1 <= len f2 ) } by A75, ZFMISC_1:32;

{ (LSeg (f2,i)) where i is Nat : ( 1 <= i & i + 1 <= len f2 ) } c= {(LSeg (p0,p10)),(LSeg (p10,p1))}

hence L~ f2 = (LSeg (p0,p10)) \/ (LSeg (p10,p1)) by ZFMISC_1:75; :: thesis: ( rectangle (a,b,c,d) = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {p0,p1} & f1 /. 1 = p0 & f1 /. (len f1) = p1 & f2 /. 1 = p0 & f2 /. (len f2) = p1 )

L~ f2 = (LSeg (p0,p10)) \/ (LSeg (p10,p1)) by A80, ZFMISC_1:75;

then A81: L~ f2 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) } \/ (LSeg (p10,p1)) by A1, A3, A6, Th30

.= { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `1 = b & p `2 <= d & p `2 >= c ) } by A2, A4, A6, Th30 ;

rectangle (a,b,c,d) = ((LSeg (p0,p01)) \/ (LSeg (p01,p1))) \/ ((LSeg (p0,p10)) \/ (LSeg (p10,p1))) by A3, A4, A5, A6, SPPOL_2:def 3;

hence rectangle (a,b,c,d) = (L~ f1) \/ (L~ f2) by A47, A80, ZFMISC_1:75; :: thesis: ( (L~ f1) /\ (L~ f2) = {p0,p1} & f1 /. 1 = p0 & f1 /. (len f1) = p1 & f2 /. 1 = p0 & f2 /. (len f2) = p1 )

A86: LSeg (|[a,c]|,|[a,d]|) = { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `1 = a & p3 `2 <= d & p3 `2 >= c ) } by A2, Th30;

A87: LSeg (|[a,d]|,|[b,d]|) = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= b & p2 `1 >= a & p2 `2 = d ) } by A1, Th30;

A88: LSeg (|[a,c]|,|[b,c]|) = { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 <= b & q1 `1 >= a & q1 `2 = c ) } by A1, Th30;

A89: LSeg (|[b,c]|,|[b,d]|) = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = b & q2 `2 <= d & q2 `2 >= c ) } by A2, Th30;

A90: (LSeg (|[a,c]|,|[a,d]|)) /\ (LSeg (|[a,c]|,|[b,c]|)) = {|[a,c]|} by A1, A2, Th31;

A91: (LSeg (|[a,d]|,|[b,d]|)) /\ (LSeg (|[b,c]|,|[b,d]|)) = {|[b,d]|} by A1, A2, Th33;

thus (L~ f1) /\ (L~ f2) = (( { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) } ) /\ { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) } ) \/ (( { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) } ) /\ { p where p is Point of (TOP-REAL 2) : ( p `1 = b & p `2 <= d & p `2 >= c ) } ) by A48, A81, XBOOLE_1:23

.= (( { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) } )) \/ (( { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) } ) /\ { p where p is Point of (TOP-REAL 2) : ( p `1 = b & p `2 <= d & p `2 >= c ) } ) by XBOOLE_1:23

.= ( { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) } ) \/ (( { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 = b & p `2 <= d & p `2 >= c ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 = b & p `2 <= d & p `2 >= c ) } )) by A85, XBOOLE_1:23

.= {p0,p1} by A3, A4, A86, A87, A88, A89, A90, A91, A95, ENUMSET1:1 ; :: thesis: ( f1 /. 1 = p0 & f1 /. (len f1) = p1 & f2 /. 1 = p0 & f2 /. (len f2) = p1 )

thus ( f1 /. 1 = p0 & f1 /. (len f1) = p1 & f2 /. 1 = p0 & f2 /. (len f2) = p1 ) by A7, A8, A15, A49, FINSEQ_4:18; :: thesis: verum

for p0, p1, p01, p10 being Point of (TOP-REAL 2) st a < b & c < d & p0 = |[a,c]| & p1 = |[b,d]| & p01 = |[a,d]| & p10 = |[b,c]| & f1 = <*p0,p01,p1*> & f2 = <*p0,p10,p1*> holds

( f1 is being_S-Seq & L~ f1 = (LSeg (p0,p01)) \/ (LSeg (p01,p1)) & f2 is being_S-Seq & L~ f2 = (LSeg (p0,p10)) \/ (LSeg (p10,p1)) & rectangle (a,b,c,d) = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {p0,p1} & f1 /. 1 = p0 & f1 /. (len f1) = p1 & f2 /. 1 = p0 & f2 /. (len f2) = p1 )

let f1, f2 be FinSequence of (TOP-REAL 2); :: thesis: for p0, p1, p01, p10 being Point of (TOP-REAL 2) st a < b & c < d & p0 = |[a,c]| & p1 = |[b,d]| & p01 = |[a,d]| & p10 = |[b,c]| & f1 = <*p0,p01,p1*> & f2 = <*p0,p10,p1*> holds

( f1 is being_S-Seq & L~ f1 = (LSeg (p0,p01)) \/ (LSeg (p01,p1)) & f2 is being_S-Seq & L~ f2 = (LSeg (p0,p10)) \/ (LSeg (p10,p1)) & rectangle (a,b,c,d) = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {p0,p1} & f1 /. 1 = p0 & f1 /. (len f1) = p1 & f2 /. 1 = p0 & f2 /. (len f2) = p1 )

let p0, p1, p01, p10 be Point of (TOP-REAL 2); :: thesis: ( a < b & c < d & p0 = |[a,c]| & p1 = |[b,d]| & p01 = |[a,d]| & p10 = |[b,c]| & f1 = <*p0,p01,p1*> & f2 = <*p0,p10,p1*> implies ( f1 is being_S-Seq & L~ f1 = (LSeg (p0,p01)) \/ (LSeg (p01,p1)) & f2 is being_S-Seq & L~ f2 = (LSeg (p0,p10)) \/ (LSeg (p10,p1)) & rectangle (a,b,c,d) = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {p0,p1} & f1 /. 1 = p0 & f1 /. (len f1) = p1 & f2 /. 1 = p0 & f2 /. (len f2) = p1 ) )

assume that

A1: a < b and

A2: c < d and

A3: p0 = |[a,c]| and

A4: p1 = |[b,d]| and

A5: p01 = |[a,d]| and

A6: p10 = |[b,c]| and

A7: f1 = <*p0,p01,p1*> and

A8: f2 = <*p0,p10,p1*> ; :: thesis: ( f1 is being_S-Seq & L~ f1 = (LSeg (p0,p01)) \/ (LSeg (p01,p1)) & f2 is being_S-Seq & L~ f2 = (LSeg (p0,p10)) \/ (LSeg (p10,p1)) & rectangle (a,b,c,d) = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {p0,p1} & f1 /. 1 = p0 & f1 /. (len f1) = p1 & f2 /. 1 = p0 & f2 /. (len f2) = p1 )

set P = rectangle (a,b,c,d);

set L1 = { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } ;

set L2 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) } ;

set L3 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) } ;

set L4 = { p where p is Point of (TOP-REAL 2) : ( p `1 = b & p `2 <= d & p `2 >= c ) } ;

A9: p1 `1 = b by A4, EUCLID:52;

A10: p1 `2 = d by A4, EUCLID:52;

A11: p10 `1 = b by A6, EUCLID:52;

A12: p10 `2 = c by A6, EUCLID:52;

A13: p0 `1 = a by A3, EUCLID:52;

A14: p0 `2 = c by A3, EUCLID:52;

A15: len f1 = 1 + 2 by A7, FINSEQ_1:45;

A16: f1 /. 1 = p0 by A7, FINSEQ_4:18;

A17: f1 /. 2 = p01 by A7, FINSEQ_4:18;

A18: f1 /. 3 = p1 by A7, FINSEQ_4:18;

thus f1 is being_S-Seq :: thesis: ( L~ f1 = (LSeg (p0,p01)) \/ (LSeg (p01,p1)) & f2 is being_S-Seq & L~ f2 = (LSeg (p0,p10)) \/ (LSeg (p10,p1)) & rectangle (a,b,c,d) = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {p0,p1} & f1 /. 1 = p0 & f1 /. (len f1) = p1 & f2 /. 1 = p0 & f2 /. (len f2) = p1 )

proof

A40:
1 + 1 in Seg (len f1)
by A15, FINSEQ_1:1;
A19:
p0 <> p01
by A2, A5, A14, EUCLID:52;

p01 <> p1 by A1, A5, A9, EUCLID:52;

hence f1 is one-to-one by A1, A7, A9, A13, A19, FINSEQ_3:95; :: according to TOPREAL1:def 8 :: thesis: ( 2 <= len f1 & f1 is unfolded & f1 is s.n.c. & f1 is special )

thus len f1 >= 2 by A15; :: thesis: ( f1 is unfolded & f1 is s.n.c. & f1 is special )

thus f1 is unfolded :: thesis: ( f1 is s.n.c. & f1 is special )

assume that

A35: 1 <= i and

A36: i + 1 <= len f1 ; :: thesis: ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 )

A37: i <= 1 + 1 by A15, A36, XREAL_1:6;

end;p01 <> p1 by A1, A5, A9, EUCLID:52;

hence f1 is one-to-one by A1, A7, A9, A13, A19, FINSEQ_3:95; :: according to TOPREAL1:def 8 :: thesis: ( 2 <= len f1 & f1 is unfolded & f1 is s.n.c. & f1 is special )

thus len f1 >= 2 by A15; :: thesis: ( f1 is unfolded & f1 is s.n.c. & f1 is special )

thus f1 is unfolded :: thesis: ( f1 is s.n.c. & f1 is special )

proof

thus
f1 is s.n.c.
:: thesis: f1 is special
let i be Nat; :: according to TOPREAL1:def 6 :: thesis: ( not 1 <= i or not i + 2 <= len f1 or (LSeg (f1,i)) /\ (LSeg (f1,(i + 1))) = {(f1 /. (i + 1))} )

assume that

A20: 1 <= i and

A21: i + 2 <= len f1 ; :: thesis: (LSeg (f1,i)) /\ (LSeg (f1,(i + 1))) = {(f1 /. (i + 1))}

i <= 1 by A15, A21, XREAL_1:6;

then A22: i = 1 by A20, XXREAL_0:1;

reconsider n2 = 1 + 1 as Nat ;

n2 in Seg (len f1) by A15, FINSEQ_1:1;

then A23: LSeg (f1,1) = LSeg (p0,p01) by A15, A16, A17, TOPREAL1:def 3;

A24: LSeg (f1,n2) = LSeg (p01,p1) by A15, A17, A18, TOPREAL1:def 3;

for x being object holds

( x in (LSeg (p0,p01)) /\ (LSeg (p01,p1)) iff x = p01 )

end;assume that

A20: 1 <= i and

A21: i + 2 <= len f1 ; :: thesis: (LSeg (f1,i)) /\ (LSeg (f1,(i + 1))) = {(f1 /. (i + 1))}

i <= 1 by A15, A21, XREAL_1:6;

then A22: i = 1 by A20, XXREAL_0:1;

reconsider n2 = 1 + 1 as Nat ;

n2 in Seg (len f1) by A15, FINSEQ_1:1;

then A23: LSeg (f1,1) = LSeg (p0,p01) by A15, A16, A17, TOPREAL1:def 3;

A24: LSeg (f1,n2) = LSeg (p01,p1) by A15, A17, A18, TOPREAL1:def 3;

for x being object holds

( x in (LSeg (p0,p01)) /\ (LSeg (p01,p1)) iff x = p01 )

proof

hence
(LSeg (f1,i)) /\ (LSeg (f1,(i + 1))) = {(f1 /. (i + 1))}
by A17, A22, A23, A24, TARSKI:def 1; :: thesis: verum
let x be object ; :: thesis: ( x in (LSeg (p0,p01)) /\ (LSeg (p01,p1)) iff x = p01 )

thus ( x in (LSeg (p0,p01)) /\ (LSeg (p01,p1)) implies x = p01 ) :: thesis: ( x = p01 implies x in (LSeg (p0,p01)) /\ (LSeg (p01,p1)) )

then A32: x in LSeg (p0,p01) by RLTOPSP1:68;

x in LSeg (p01,p1) by A31, RLTOPSP1:68;

hence x in (LSeg (p0,p01)) /\ (LSeg (p01,p1)) by A32, XBOOLE_0:def 4; :: thesis: verum

end;thus ( x in (LSeg (p0,p01)) /\ (LSeg (p01,p1)) implies x = p01 ) :: thesis: ( x = p01 implies x in (LSeg (p0,p01)) /\ (LSeg (p01,p1)) )

proof

assume A31:
x = p01
; :: thesis: x in (LSeg (p0,p01)) /\ (LSeg (p01,p1))
assume A25:
x in (LSeg (p0,p01)) /\ (LSeg (p01,p1))
; :: thesis: x = p01

then A26: x in LSeg (p0,p01) by XBOOLE_0:def 4;

A27: x in LSeg (p01,p1) by A25, XBOOLE_0:def 4;

A28: x in { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } by A2, A3, A5, A26, Th30;

A29: x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= b & p2 `1 >= a & p2 `2 = d ) } by A1, A4, A5, A27, Th30;

A30: ex p being Point of (TOP-REAL 2) st

( p = x & p `1 = a & p `2 <= d & p `2 >= c ) by A28;

ex p2 being Point of (TOP-REAL 2) st

( p2 = x & p2 `1 <= b & p2 `1 >= a & p2 `2 = d ) by A29;

hence x = p01 by A5, A30, EUCLID:53; :: thesis: verum

end;then A26: x in LSeg (p0,p01) by XBOOLE_0:def 4;

A27: x in LSeg (p01,p1) by A25, XBOOLE_0:def 4;

A28: x in { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } by A2, A3, A5, A26, Th30;

A29: x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= b & p2 `1 >= a & p2 `2 = d ) } by A1, A4, A5, A27, Th30;

A30: ex p being Point of (TOP-REAL 2) st

( p = x & p `1 = a & p `2 <= d & p `2 >= c ) by A28;

ex p2 being Point of (TOP-REAL 2) st

( p2 = x & p2 `1 <= b & p2 `1 >= a & p2 `2 = d ) by A29;

hence x = p01 by A5, A30, EUCLID:53; :: thesis: verum

then A32: x in LSeg (p0,p01) by RLTOPSP1:68;

x in LSeg (p01,p1) by A31, RLTOPSP1:68;

hence x in (LSeg (p0,p01)) /\ (LSeg (p01,p1)) by A32, XBOOLE_0:def 4; :: thesis: verum

proof

let i be Nat; :: according to TOPREAL1:def 5 :: thesis: ( not 1 <= i or not i + 1 <= len f1 or (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 )
let i, j be Nat; :: according to TOPREAL1:def 7 :: thesis: ( j <= i + 1 or LSeg (f1,i) misses LSeg (f1,j) )

assume A33: i + 1 < j ; :: thesis: LSeg (f1,i) misses LSeg (f1,j)

end;assume A33: i + 1 < j ; :: thesis: LSeg (f1,i) misses LSeg (f1,j)

now :: thesis: (LSeg (f1,i)) /\ (LSeg (f1,j)) = {} end;

hence
(LSeg (f1,i)) /\ (LSeg (f1,j)) = {}
; :: according to XBOOLE_0:def 7 :: thesis: verumper cases
( 1 <= i or not 1 <= i or not i + 1 <= len f1 )
;

end;

suppose
1 <= i
; :: thesis: (LSeg (f1,i)) /\ (LSeg (f1,j)) = {}

then A34:
1 + 1 <= i + 1
by XREAL_1:6;

end;now :: thesis: ( ( 1 <= j & j + 1 <= len f1 & contradiction ) or ( ( not 1 <= j or not j + 1 <= len f1 ) & (LSeg (f1,i)) /\ (LSeg (f1,j)) = {} ) )

hence
(LSeg (f1,i)) /\ (LSeg (f1,j)) = {}
; :: thesis: verumend;

assume that

A35: 1 <= i and

A36: i + 1 <= len f1 ; :: thesis: ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 )

A37: i <= 1 + 1 by A15, A36, XREAL_1:6;

now :: thesis: ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 )end;

hence
( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 )
; :: thesis: verumper cases
( i = 1 or i = 2 )
by A35, A37, NAT_1:9;

end;

suppose A38:
i = 1
; :: thesis: ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 )

then (f1 /. i) `1 =
p0 `1
by A7, FINSEQ_4:18

.= a by A3, EUCLID:52

.= (f1 /. (i + 1)) `1 by A5, A17, A38, EUCLID:52 ;

hence ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 ) ; :: thesis: verum

end;.= a by A3, EUCLID:52

.= (f1 /. (i + 1)) `1 by A5, A17, A38, EUCLID:52 ;

hence ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 ) ; :: thesis: verum

suppose A39:
i = 2
; :: thesis: ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 )

then (f1 /. i) `2 =
p01 `2
by A7, FINSEQ_4:18

.= d by A5, EUCLID:52

.= (f1 /. (i + 1)) `2 by A4, A18, A39, EUCLID:52 ;

hence ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 ) ; :: thesis: verum

end;.= d by A5, EUCLID:52

.= (f1 /. (i + 1)) `2 by A4, A18, A39, EUCLID:52 ;

hence ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 ) ; :: thesis: verum

A41: 1 + 1 <= len f1 by A15;

LSeg (p0,p01) = LSeg (f1,1) by A15, A16, A17, A40, TOPREAL1:def 3;

then A42: LSeg (p0,p01) in { (LSeg (f1,i)) where i is Nat : ( 1 <= i & i + 1 <= len f1 ) } by A41;

LSeg (p01,p1) = LSeg (f1,2) by A15, A17, A18, TOPREAL1:def 3;

then LSeg (p01,p1) in { (LSeg (f1,i)) where i is Nat : ( 1 <= i & i + 1 <= len f1 ) } by A15;

then A43: {(LSeg (p0,p01)),(LSeg (p01,p1))} c= { (LSeg (f1,i)) where i is Nat : ( 1 <= i & i + 1 <= len f1 ) } by A42, ZFMISC_1:32;

{ (LSeg (f1,i)) where i is Nat : ( 1 <= i & i + 1 <= len f1 ) } c= {(LSeg (p0,p01)),(LSeg (p01,p1))}

proof

then
L~ f1 = union {(LSeg (p0,p01)),(LSeg (p01,p1))}
by A43, XBOOLE_0:def 10;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (LSeg (f1,i)) where i is Nat : ( 1 <= i & i + 1 <= len f1 ) } or a in {(LSeg (p0,p01)),(LSeg (p01,p1))} )

assume a in { (LSeg (f1,i)) where i is Nat : ( 1 <= i & i + 1 <= len f1 ) } ; :: thesis: a in {(LSeg (p0,p01)),(LSeg (p01,p1))}

then consider i being Nat such that

A44: a = LSeg (f1,i) and

A45: 1 <= i and

A46: i + 1 <= len f1 ;

i + 1 <= 2 + 1 by A7, A46, FINSEQ_1:45;

then i <= 1 + 1 by XREAL_1:6;

then ( i = 1 or i = 2 ) by A45, NAT_1:9;

then ( a = LSeg (p0,p01) or a = LSeg (p01,p1) ) by A16, A17, A18, A44, A46, TOPREAL1:def 3;

hence a in {(LSeg (p0,p01)),(LSeg (p01,p1))} by TARSKI:def 2; :: thesis: verum

end;assume a in { (LSeg (f1,i)) where i is Nat : ( 1 <= i & i + 1 <= len f1 ) } ; :: thesis: a in {(LSeg (p0,p01)),(LSeg (p01,p1))}

then consider i being Nat such that

A44: a = LSeg (f1,i) and

A45: 1 <= i and

A46: i + 1 <= len f1 ;

i + 1 <= 2 + 1 by A7, A46, FINSEQ_1:45;

then i <= 1 + 1 by XREAL_1:6;

then ( i = 1 or i = 2 ) by A45, NAT_1:9;

then ( a = LSeg (p0,p01) or a = LSeg (p01,p1) ) by A16, A17, A18, A44, A46, TOPREAL1:def 3;

hence a in {(LSeg (p0,p01)),(LSeg (p01,p1))} by TARSKI:def 2; :: thesis: verum

hence A47: L~ f1 = (LSeg (p0,p01)) \/ (LSeg (p01,p1)) by ZFMISC_1:75; :: thesis: ( f2 is being_S-Seq & L~ f2 = (LSeg (p0,p10)) \/ (LSeg (p10,p1)) & rectangle (a,b,c,d) = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {p0,p1} & f1 /. 1 = p0 & f1 /. (len f1) = p1 & f2 /. 1 = p0 & f2 /. (len f2) = p1 )

then A48: L~ f1 = { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } \/ (LSeg (p01,p1)) by A2, A3, A5, Th30

.= { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) } by A1, A4, A5, Th30 ;

A49: len f2 = 1 + 2 by A8, FINSEQ_1:45;

A50: f2 /. 1 = p0 by A8, FINSEQ_4:18;

A51: f2 /. 2 = p10 by A8, FINSEQ_4:18;

A52: f2 /. 3 = p1 by A8, FINSEQ_4:18;

thus f2 is being_S-Seq :: thesis: ( L~ f2 = (LSeg (p0,p10)) \/ (LSeg (p10,p1)) & rectangle (a,b,c,d) = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {p0,p1} & f1 /. 1 = p0 & f1 /. (len f1) = p1 & f2 /. 1 = p0 & f2 /. (len f2) = p1 )

proof

A73:
1 + 1 in Seg (len f2)
by A49, FINSEQ_1:1;
thus
f2 is one-to-one
by A1, A2, A8, A9, A10, A11, A12, A13, FINSEQ_3:95; :: according to TOPREAL1:def 8 :: thesis: ( 2 <= len f2 & f2 is unfolded & f2 is s.n.c. & f2 is special )

thus len f2 >= 2 by A49; :: thesis: ( f2 is unfolded & f2 is s.n.c. & f2 is special )

thus f2 is unfolded :: thesis: ( f2 is s.n.c. & f2 is special )

assume that

A68: 1 <= i and

A69: i + 1 <= len f2 ; :: thesis: ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 )

A70: i <= 1 + 1 by A49, A69, XREAL_1:6;

end;thus len f2 >= 2 by A49; :: thesis: ( f2 is unfolded & f2 is s.n.c. & f2 is special )

thus f2 is unfolded :: thesis: ( f2 is s.n.c. & f2 is special )

proof

thus
f2 is s.n.c.
:: thesis: f2 is special
let i be Nat; :: according to TOPREAL1:def 6 :: thesis: ( not 1 <= i or not i + 2 <= len f2 or (LSeg (f2,i)) /\ (LSeg (f2,(i + 1))) = {(f2 /. (i + 1))} )

assume that

A53: 1 <= i and

A54: i + 2 <= len f2 ; :: thesis: (LSeg (f2,i)) /\ (LSeg (f2,(i + 1))) = {(f2 /. (i + 1))}

i <= 1 by A49, A54, XREAL_1:6;

then A55: i = 1 by A53, XXREAL_0:1;

1 + 1 in Seg (len f2) by A49, FINSEQ_1:1;

then A56: LSeg (f2,1) = LSeg (p0,p10) by A49, A50, A51, TOPREAL1:def 3;

A57: LSeg (f2,(1 + 1)) = LSeg (p10,p1) by A49, A51, A52, TOPREAL1:def 3;

for x being object holds

( x in (LSeg (p0,p10)) /\ (LSeg (p10,p1)) iff x = p10 )

end;assume that

A53: 1 <= i and

A54: i + 2 <= len f2 ; :: thesis: (LSeg (f2,i)) /\ (LSeg (f2,(i + 1))) = {(f2 /. (i + 1))}

i <= 1 by A49, A54, XREAL_1:6;

then A55: i = 1 by A53, XXREAL_0:1;

1 + 1 in Seg (len f2) by A49, FINSEQ_1:1;

then A56: LSeg (f2,1) = LSeg (p0,p10) by A49, A50, A51, TOPREAL1:def 3;

A57: LSeg (f2,(1 + 1)) = LSeg (p10,p1) by A49, A51, A52, TOPREAL1:def 3;

for x being object holds

( x in (LSeg (p0,p10)) /\ (LSeg (p10,p1)) iff x = p10 )

proof

hence
(LSeg (f2,i)) /\ (LSeg (f2,(i + 1))) = {(f2 /. (i + 1))}
by A51, A55, A56, A57, TARSKI:def 1; :: thesis: verum
let x be object ; :: thesis: ( x in (LSeg (p0,p10)) /\ (LSeg (p10,p1)) iff x = p10 )

thus ( x in (LSeg (p0,p10)) /\ (LSeg (p10,p1)) implies x = p10 ) :: thesis: ( x = p10 implies x in (LSeg (p0,p10)) /\ (LSeg (p10,p1)) )

then A65: x in LSeg (p0,p10) by RLTOPSP1:68;

x in LSeg (p10,p1) by A64, RLTOPSP1:68;

hence x in (LSeg (p0,p10)) /\ (LSeg (p10,p1)) by A65, XBOOLE_0:def 4; :: thesis: verum

end;thus ( x in (LSeg (p0,p10)) /\ (LSeg (p10,p1)) implies x = p10 ) :: thesis: ( x = p10 implies x in (LSeg (p0,p10)) /\ (LSeg (p10,p1)) )

proof

assume A64:
x = p10
; :: thesis: x in (LSeg (p0,p10)) /\ (LSeg (p10,p1))
assume A58:
x in (LSeg (p0,p10)) /\ (LSeg (p10,p1))
; :: thesis: x = p10

then A59: x in LSeg (p0,p10) by XBOOLE_0:def 4;

A60: x in LSeg (p10,p1) by A58, XBOOLE_0:def 4;

A61: x in { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) } by A1, A3, A6, A59, Th30;

A62: x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = b & p2 `2 <= d & p2 `2 >= c ) } by A2, A4, A6, A60, Th30;

A63: ex p being Point of (TOP-REAL 2) st

( p = x & p `1 <= b & p `1 >= a & p `2 = c ) by A61;

ex p2 being Point of (TOP-REAL 2) st

( p2 = x & p2 `1 = b & p2 `2 <= d & p2 `2 >= c ) by A62;

hence x = p10 by A6, A63, EUCLID:53; :: thesis: verum

end;then A59: x in LSeg (p0,p10) by XBOOLE_0:def 4;

A60: x in LSeg (p10,p1) by A58, XBOOLE_0:def 4;

A61: x in { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) } by A1, A3, A6, A59, Th30;

A62: x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = b & p2 `2 <= d & p2 `2 >= c ) } by A2, A4, A6, A60, Th30;

A63: ex p being Point of (TOP-REAL 2) st

( p = x & p `1 <= b & p `1 >= a & p `2 = c ) by A61;

ex p2 being Point of (TOP-REAL 2) st

( p2 = x & p2 `1 = b & p2 `2 <= d & p2 `2 >= c ) by A62;

hence x = p10 by A6, A63, EUCLID:53; :: thesis: verum

then A65: x in LSeg (p0,p10) by RLTOPSP1:68;

x in LSeg (p10,p1) by A64, RLTOPSP1:68;

hence x in (LSeg (p0,p10)) /\ (LSeg (p10,p1)) by A65, XBOOLE_0:def 4; :: thesis: verum

proof

let i be Nat; :: according to TOPREAL1:def 5 :: thesis: ( not 1 <= i or not i + 1 <= len f2 or (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 )
let i, j be Nat; :: according to TOPREAL1:def 7 :: thesis: ( j <= i + 1 or LSeg (f2,i) misses LSeg (f2,j) )

assume A66: i + 1 < j ; :: thesis: LSeg (f2,i) misses LSeg (f2,j)

end;assume A66: i + 1 < j ; :: thesis: LSeg (f2,i) misses LSeg (f2,j)

now :: thesis: (LSeg (f2,i)) /\ (LSeg (f2,j)) = {} end;

hence
(LSeg (f2,i)) /\ (LSeg (f2,j)) = {}
; :: according to XBOOLE_0:def 7 :: thesis: verumper cases
( 1 <= i or not 1 <= i or not i + 1 <= len f2 )
;

end;

suppose
1 <= i
; :: thesis: (LSeg (f2,i)) /\ (LSeg (f2,j)) = {}

then A67:
1 + 1 <= i + 1
by XREAL_1:6;

end;now :: thesis: ( ( 1 <= j & j + 1 <= len f2 & contradiction ) or ( ( not 1 <= j or not j + 1 <= len f2 ) & (LSeg (f2,i)) /\ (LSeg (f2,j)) = {} ) )

hence
(LSeg (f2,i)) /\ (LSeg (f2,j)) = {}
; :: thesis: verumend;

assume that

A68: 1 <= i and

A69: i + 1 <= len f2 ; :: thesis: ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 )

A70: i <= 1 + 1 by A49, A69, XREAL_1:6;

per cases
( i = 1 or i = 2 )
by A68, A70, NAT_1:9;

end;

suppose A71:
i = 1
; :: thesis: ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 )

then (f2 /. i) `2 =
p0 `2
by A8, FINSEQ_4:18

.= c by A3, EUCLID:52

.= (f2 /. (i + 1)) `2 by A6, A51, A71, EUCLID:52 ;

hence ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 ) ; :: thesis: verum

end;.= c by A3, EUCLID:52

.= (f2 /. (i + 1)) `2 by A6, A51, A71, EUCLID:52 ;

hence ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 ) ; :: thesis: verum

suppose A72:
i = 2
; :: thesis: ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 )

then (f2 /. i) `1 =
p10 `1
by A8, FINSEQ_4:18

.= b by A6, EUCLID:52

.= (f2 /. (i + 1)) `1 by A4, A52, A72, EUCLID:52 ;

hence ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 ) ; :: thesis: verum

end;.= b by A6, EUCLID:52

.= (f2 /. (i + 1)) `1 by A4, A52, A72, EUCLID:52 ;

hence ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 ) ; :: thesis: verum

A74: 1 + 1 <= len f2 by A49;

LSeg (p0,p10) = LSeg (f2,1) by A49, A50, A51, A73, TOPREAL1:def 3;

then A75: LSeg (p0,p10) in { (LSeg (f2,i)) where i is Nat : ( 1 <= i & i + 1 <= len f2 ) } by A74;

LSeg (p10,p1) = LSeg (f2,2) by A49, A51, A52, TOPREAL1:def 3;

then LSeg (p10,p1) in { (LSeg (f2,i)) where i is Nat : ( 1 <= i & i + 1 <= len f2 ) } by A49;

then A76: {(LSeg (p0,p10)),(LSeg (p10,p1))} c= { (LSeg (f2,i)) where i is Nat : ( 1 <= i & i + 1 <= len f2 ) } by A75, ZFMISC_1:32;

{ (LSeg (f2,i)) where i is Nat : ( 1 <= i & i + 1 <= len f2 ) } c= {(LSeg (p0,p10)),(LSeg (p10,p1))}

proof

then A80:
L~ f2 = union {(LSeg (p0,p10)),(LSeg (p10,p1))}
by A76, XBOOLE_0:def 10;
let ax be object ; :: according to TARSKI:def 3 :: thesis: ( not ax in { (LSeg (f2,i)) where i is Nat : ( 1 <= i & i + 1 <= len f2 ) } or ax in {(LSeg (p0,p10)),(LSeg (p10,p1))} )

assume ax in { (LSeg (f2,i)) where i is Nat : ( 1 <= i & i + 1 <= len f2 ) } ; :: thesis: ax in {(LSeg (p0,p10)),(LSeg (p10,p1))}

then consider i being Nat such that

A77: ax = LSeg (f2,i) and

A78: 1 <= i and

A79: i + 1 <= len f2 ;

i + 1 <= 2 + 1 by A8, A79, FINSEQ_1:45;

then i <= 1 + 1 by XREAL_1:6;

then ( i = 1 or i = 2 ) by A78, NAT_1:9;

then ( ax = LSeg (p0,p10) or ax = LSeg (p10,p1) ) by A50, A51, A52, A77, A79, TOPREAL1:def 3;

hence ax in {(LSeg (p0,p10)),(LSeg (p10,p1))} by TARSKI:def 2; :: thesis: verum

end;assume ax in { (LSeg (f2,i)) where i is Nat : ( 1 <= i & i + 1 <= len f2 ) } ; :: thesis: ax in {(LSeg (p0,p10)),(LSeg (p10,p1))}

then consider i being Nat such that

A77: ax = LSeg (f2,i) and

A78: 1 <= i and

A79: i + 1 <= len f2 ;

i + 1 <= 2 + 1 by A8, A79, FINSEQ_1:45;

then i <= 1 + 1 by XREAL_1:6;

then ( i = 1 or i = 2 ) by A78, NAT_1:9;

then ( ax = LSeg (p0,p10) or ax = LSeg (p10,p1) ) by A50, A51, A52, A77, A79, TOPREAL1:def 3;

hence ax in {(LSeg (p0,p10)),(LSeg (p10,p1))} by TARSKI:def 2; :: thesis: verum

hence L~ f2 = (LSeg (p0,p10)) \/ (LSeg (p10,p1)) by ZFMISC_1:75; :: thesis: ( rectangle (a,b,c,d) = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {p0,p1} & f1 /. 1 = p0 & f1 /. (len f1) = p1 & f2 /. 1 = p0 & f2 /. (len f2) = p1 )

L~ f2 = (LSeg (p0,p10)) \/ (LSeg (p10,p1)) by A80, ZFMISC_1:75;

then A81: L~ f2 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) } \/ (LSeg (p10,p1)) by A1, A3, A6, Th30

.= { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `1 = b & p `2 <= d & p `2 >= c ) } by A2, A4, A6, Th30 ;

rectangle (a,b,c,d) = ((LSeg (p0,p01)) \/ (LSeg (p01,p1))) \/ ((LSeg (p0,p10)) \/ (LSeg (p10,p1))) by A3, A4, A5, A6, SPPOL_2:def 3;

hence rectangle (a,b,c,d) = (L~ f1) \/ (L~ f2) by A47, A80, ZFMISC_1:75; :: thesis: ( (L~ f1) /\ (L~ f2) = {p0,p1} & f1 /. 1 = p0 & f1 /. (len f1) = p1 & f2 /. 1 = p0 & f2 /. (len f2) = p1 )

now :: thesis: not { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) } meets { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) }

then A85:
{ p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) } = {}
;assume
{ p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) } meets { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) }
; :: thesis: contradiction

then consider x being object such that

A82: x in { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) } and

A83: x in { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) } by XBOOLE_0:3;

A84: ex p being Point of (TOP-REAL 2) st

( p = x & p `1 <= b & p `1 >= a & p `2 = d ) by A82;

ex p2 being Point of (TOP-REAL 2) st

( p2 = x & p2 `1 <= b & p2 `1 >= a & p2 `2 = c ) by A83;

hence contradiction by A2, A84; :: thesis: verum

end;then consider x being object such that

A82: x in { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) } and

A83: x in { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) } by XBOOLE_0:3;

A84: ex p being Point of (TOP-REAL 2) st

( p = x & p `1 <= b & p `1 >= a & p `2 = d ) by A82;

ex p2 being Point of (TOP-REAL 2) st

( p2 = x & p2 `1 <= b & p2 `1 >= a & p2 `2 = c ) by A83;

hence contradiction by A2, A84; :: thesis: verum

A86: LSeg (|[a,c]|,|[a,d]|) = { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `1 = a & p3 `2 <= d & p3 `2 >= c ) } by A2, Th30;

A87: LSeg (|[a,d]|,|[b,d]|) = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= b & p2 `1 >= a & p2 `2 = d ) } by A1, Th30;

A88: LSeg (|[a,c]|,|[b,c]|) = { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 <= b & q1 `1 >= a & q1 `2 = c ) } by A1, Th30;

A89: LSeg (|[b,c]|,|[b,d]|) = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = b & q2 `2 <= d & q2 `2 >= c ) } by A2, Th30;

A90: (LSeg (|[a,c]|,|[a,d]|)) /\ (LSeg (|[a,c]|,|[b,c]|)) = {|[a,c]|} by A1, A2, Th31;

A91: (LSeg (|[a,d]|,|[b,d]|)) /\ (LSeg (|[b,c]|,|[b,d]|)) = {|[b,d]|} by A1, A2, Th33;

now :: thesis: not { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } meets { p where p is Point of (TOP-REAL 2) : ( p `1 = b & p `2 <= d & p `2 >= c ) }

then A95:
{ p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 = b & p `2 <= d & p `2 >= c ) } = {}
;assume
{ p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } meets { p where p is Point of (TOP-REAL 2) : ( p `1 = b & p `2 <= d & p `2 >= c ) }
; :: thesis: contradiction

then consider x being object such that

A92: x in { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } and

A93: x in { p where p is Point of (TOP-REAL 2) : ( p `1 = b & p `2 <= d & p `2 >= c ) } by XBOOLE_0:3;

A94: ex p being Point of (TOP-REAL 2) st

( p = x & p `1 = a & p `2 <= d & p `2 >= c ) by A92;

ex p2 being Point of (TOP-REAL 2) st

( p2 = x & p2 `1 = b & p2 `2 <= d & p2 `2 >= c ) by A93;

hence contradiction by A1, A94; :: thesis: verum

end;then consider x being object such that

A92: x in { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } and

A93: x in { p where p is Point of (TOP-REAL 2) : ( p `1 = b & p `2 <= d & p `2 >= c ) } by XBOOLE_0:3;

A94: ex p being Point of (TOP-REAL 2) st

( p = x & p `1 = a & p `2 <= d & p `2 >= c ) by A92;

ex p2 being Point of (TOP-REAL 2) st

( p2 = x & p2 `1 = b & p2 `2 <= d & p2 `2 >= c ) by A93;

hence contradiction by A1, A94; :: thesis: verum

thus (L~ f1) /\ (L~ f2) = (( { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) } ) /\ { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) } ) \/ (( { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) } ) /\ { p where p is Point of (TOP-REAL 2) : ( p `1 = b & p `2 <= d & p `2 >= c ) } ) by A48, A81, XBOOLE_1:23

.= (( { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) } )) \/ (( { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) } ) /\ { p where p is Point of (TOP-REAL 2) : ( p `1 = b & p `2 <= d & p `2 >= c ) } ) by XBOOLE_1:23

.= ( { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) } ) \/ (( { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 = b & p `2 <= d & p `2 >= c ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 = b & p `2 <= d & p `2 >= c ) } )) by A85, XBOOLE_1:23

.= {p0,p1} by A3, A4, A86, A87, A88, A89, A90, A91, A95, ENUMSET1:1 ; :: thesis: ( f1 /. 1 = p0 & f1 /. (len f1) = p1 & f2 /. 1 = p0 & f2 /. (len f2) = p1 )

thus ( f1 /. 1 = p0 & f1 /. (len f1) = p1 & f2 /. 1 = p0 & f2 /. (len f2) = p1 ) by A7, A8, A15, A49, FINSEQ_4:18; :: thesis: verum