let a, b, c, d be real number ; :: thesis:
let f1, f2 be FinSequence of (TOP-REAL 2); :: thesis:
let p0, p1, p01, p10 be Point of (TOP-REAL 2); :: thesis:
assume A1: ( a < b & c < d & p0 = |[a,c]| & p1 = |[b,d]| & p01 = |[a,d]| & p10 = |[b,c]| & f1 = <*p0,p01,p1*> & f2 = <*p0,p10,p1*> ) ; :: thesis:
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 ) } ;
A2: ( p1 `1 = b & p1 `2 = d ) by A1, EUCLID:56;
A3: ( p10 `1 = b & p10 `2 = c ) by A1, EUCLID:56;
A4: ( p0 `1 = a & p0 `2 = c ) by A1, EUCLID:56;
A5: len f1 = 1 + 2 by A1, FINSEQ_1:62;
A6: ( f1 /. 1 = p0 & f1 /. 2 = p01 & f1 /. 3 = p1 ) by A1, FINSEQ_4:27;
thus f1 is being_S-Seq :: thesis:

proof

( p0 <> p01 & p01 <> p1 & p0 <> p1 ) by A1, A2, A4, EUCLID:56;
hence f1 is one-to-one by A1, FINSEQ_3:104; :: according to TOPREAL1:def 10 :: thesis:
thus len f1 >= 2 by A5; :: thesis:
thus f1 is unfolded :: thesis:

proof

let i be Nat; :: according to TOPREAL1:def 8 :: thesis:
assume A7: ( 1 <= i & i + 2 <= len f1 ) ; :: thesis:
then i <= 1 by A5, XREAL_1:8;
then A8: i = 1 by A7, XXREAL_0:1;
reconsider n2 = 1 + 1 as Element of NAT ;
n2 in Seg (len f1) by A5, FINSEQ_1:3;
then A9: ( LSeg f1,1 = LSeg p0,p01 & LSeg f1,n2 = LSeg p01,p1 ) by A5, A6, TOPREAL1:def 5;
for x being set holds
( x in (LSeg p0,p01) /\ (LSeg p01,p1) iff x = p01 )

proof

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

proof

assume x in (LSeg p0,p01) /\ (LSeg p01,p1) ; :: thesis:
then ( x in LSeg p0,p01 & x in LSeg p01,p1 ) by XBOOLE_0:def 4;
then A10: ( x in { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } & x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= b & p2 `1 >= a & p2 `2 = d ) } ) by A1, Th39;
then A11: ex p being Point of (TOP-REAL 2) st
( p = x & p `1 = a & p `2 <= d & p `2 >= c ) ;
ex p2 being Point of (TOP-REAL 2) st
( p2 = x & p2 `1 <= b & p2 `1 >= a & p2 `2 = d ) by A10;
hence x = p01 by A1, A11, EUCLID:57; :: thesis:

end;

assume x = p01 ; :: thesis:
then ( x in LSeg p0,p01 & x in LSeg p01,p1 ) by RLTOPSP1:69;
hence x in (LSeg p0,p01) /\ (LSeg p01,p1) by XBOOLE_0:def 4; :: thesis:

end;

hence (LSeg f1,i) /\ (LSeg f1,(i + 1)) = {(f1 /. (i + 1))} by A6, A8, A9, TARSKI:def 1; :: thesis:

end;

thus f1 is s.n.c. :: thesis:

proof

let i, j be Nat; :: according to TOPREAL1:def 9 :: thesis:
assume A12: i + 1 < j ; :: thesis:

now

per cases ;

suppose 1 <= i ; :: thesis:

then A13: 1 + 1 <= i + 1 by XREAL_1:8;

now

per cases ;

case ( 1 <= j & j + 1 <= len f1 ) ; :: thesis:

then j <= 2 by A5, XREAL_1:8;
hence contradiction by A12, A13, XXREAL_0:2; :: thesis:

end;

case ( not 1 <= j or not j + 1 <= len f1 ) ; :: thesis:

then LSeg f1,j = {} by TOPREAL1:def 5;
hence (LSeg f1,i) /\ (LSeg f1,j) = {} ; :: thesis:

end;

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

end;

suppose ( not 1 <= i or not i + 1 <= len f1 ) ; :: thesis:

then LSeg f1,i = {} by TOPREAL1:def 5;
hence (LSeg f1,i) /\ (LSeg f1,j) = {} ; :: thesis:

end;

hence (LSeg f1,i) /\ (LSeg f1,j) = {} ; :: according to XBOOLE_0:def 7 :: thesis:

end;

let i be Nat; :: according to TOPREAL1:def 7 :: thesis:
assume A14: ( 1 <= i & i + 1 <= len f1 ) ; :: thesis:
then A15: i <= 1 + 1 by A5, XREAL_1:8;

now

per cases by A14, A15, NAT_1:9;

suppose A16: i = 1 ; :: thesis:

then (f1 /. i) `1 = p0 `1 by A1, FINSEQ_4:27
.= a by A1, EUCLID:56
.= (f1 /. (i + 1)) `1 by A1, A6, A16, EUCLID:56 ;
hence ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 ) ; :: thesis:

end;

suppose A17: i = 2 ; :: thesis:

then (f1 /. i) `2 = p01 `2 by A1, FINSEQ_4:27
.= d by A1, EUCLID:56
.= (f1 /. (i + 1)) `2 by A1, A6, A17, EUCLID:56 ;
hence ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 ) ; :: thesis:

end;

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

end;

L~ f1 = union {(LSeg p0,p01),(LSeg p01,p1)}

proof

( len f1 = 2 + 1 & 1 + 1 in Seg (len f1) ) by A5, FINSEQ_1:3;
then ( 1 + 1 <= len f1 & LSeg p0,p01 = LSeg f1,1 ) by A6, TOPREAL1:def 5;
then A18: LSeg p0,p01 in { (LSeg f1,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f1 ) } ;
( 2 + 1 <= len f1 & LSeg p01,p1 = LSeg f1,2 ) by A5, A6, TOPREAL1:def 5;
then LSeg p01,p1 in { (LSeg f1,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f1 ) } ;
then A19: {(LSeg p0,p01),(LSeg p01,p1)} c= { (LSeg f1,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f1 ) } by A18, ZFMISC_1:38;
{ (LSeg f1,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f1 ) } c= {(LSeg p0,p01),(LSeg p01,p1)}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in { (LSeg f1,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f1 ) } ; :: thesis:
then consider i being Element of NAT such that
A20: ( a = LSeg f1,i & 1 <= i & i + 1 <= len f1 ) ;
i + 1 <= 2 + 1 by A1, A20, FINSEQ_1:62;
then i <= 1 + 1 by XREAL_1:8;
then ( i = 1 or i = 2 ) by A20, NAT_1:9;
then ( a = LSeg p0,p01 or a = LSeg p01,p1 ) by A6, A20, TOPREAL1:def 5;
hence a in {(LSeg p0,p01),(LSeg p01,p1)} by TARSKI:def 2; :: thesis:

end;

hence L~ f1 = union {(LSeg p0,p01),(LSeg p01,p1)} by A19, XBOOLE_0:def 10; :: thesis:

end;

hence A21: L~ f1 = (LSeg p0,p01) \/ (LSeg p01,p1) by ZFMISC_1:93; :: thesis:
then A22: L~ f1 = { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } \/ (LSeg p01,p1) by A1, Th39
.= { 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, Th39 ;
A23: len f2 = 1 + 2 by A1, FINSEQ_1:62;
A24: ( f2 /. 1 = p0 & f2 /. 2 = p10 & f2 /. 3 = p1 ) by A1, FINSEQ_4:27;
thus f2 is being_S-Seq :: thesis:

proof

thus f2 is one-to-one by A1, A2, A3, A4, FINSEQ_3:104; :: according to TOPREAL1:def 10 :: thesis:
thus len f2 >= 2 by A23; :: thesis:
thus f2 is unfolded :: thesis:

proof

let i be Nat; :: according to TOPREAL1:def 8 :: thesis:
assume A25: ( 1 <= i & i + 2 <= len f2 ) ; :: thesis:
then i <= 1 by A23, XREAL_1:8;
then A26: i = 1 by A25, XXREAL_0:1;
1 + 1 in Seg (len f2) by A23, FINSEQ_1:3;
then A27: ( LSeg f2,1 = LSeg p0,p10 & LSeg f2,(1 + 1) = LSeg p10,p1 ) by A23, A24, TOPREAL1:def 5;
for x being set holds
( x in (LSeg p0,p10) /\ (LSeg p10,p1) iff x = p10 )

proof

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

proof

assume x in (LSeg p0,p10) /\ (LSeg p10,p1) ; :: thesis:
then ( x in LSeg p0,p10 & x in LSeg p10,p1 ) by XBOOLE_0:def 4;
then A28: ( x in { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) } & x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = b & p2 `2 <= d & p2 `2 >= c ) } ) by A1, Th39;
then A29: ex p being Point of (TOP-REAL 2) st
( p = x & p `1 <= b & p `1 >= a & p `2 = c ) ;
ex p2 being Point of (TOP-REAL 2) st
( p2 = x & p2 `1 = b & p2 `2 <= d & p2 `2 >= c ) by A28;
hence x = p10 by A1, A29, EUCLID:57; :: thesis:

end;

assume x = p10 ; :: thesis:
then ( x in LSeg p0,p10 & x in LSeg p10,p1 ) by RLTOPSP1:69;
hence x in (LSeg p0,p10) /\ (LSeg p10,p1) by XBOOLE_0:def 4; :: thesis:

end;

hence (LSeg f2,i) /\ (LSeg f2,(i + 1)) = {(f2 /. (i + 1))} by A24, A26, A27, TARSKI:def 1; :: thesis:

end;

thus f2 is s.n.c. :: thesis:

proof

let i, j be Nat; :: according to TOPREAL1:def 9 :: thesis:
assume A30: i + 1 < j ; :: thesis:

now

per cases ;

suppose 1 <= i ; :: thesis:

then A31: 1 + 1 <= i + 1 by XREAL_1:8;

now

per cases ;

case ( 1 <= j & j + 1 <= len f2 ) ; :: thesis:

then j <= 2 by A23, XREAL_1:8;
hence contradiction by A30, A31, XXREAL_0:2; :: thesis:

end;

case ( not 1 <= j or not j + 1 <= len f2 ) ; :: thesis:

then LSeg f2,j = {} by TOPREAL1:def 5;
hence (LSeg f2,i) /\ (LSeg f2,j) = {} ; :: thesis:

end;

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

end;

suppose ( not 1 <= i or not i + 1 <= len f2 ) ; :: thesis:

then LSeg f2,i = {} by TOPREAL1:def 5;
hence (LSeg f2,i) /\ (LSeg f2,j) = {} ; :: thesis:

end;

hence (LSeg f2,i) /\ (LSeg f2,j) = {} ; :: according to XBOOLE_0:def 7 :: thesis:

end;

let i be Nat; :: according to TOPREAL1:def 7 :: thesis:
assume A32: ( 1 <= i & i + 1 <= len f2 ) ; :: thesis:
then A33: i <= 1 + 1 by A23, XREAL_1:8;

per cases by A32, A33, NAT_1:9;

suppose A34: i = 1 ; :: thesis:

then (f2 /. i) `2 = p0 `2 by A1, FINSEQ_4:27
.= c by A1, EUCLID:56
.= (f2 /. (i + 1)) `2 by A1, A24, A34, EUCLID:56 ;
hence ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 ) ; :: thesis:

end;

suppose A35: i = 2 ; :: thesis:

then (f2 /. i) `1 = p10 `1 by A1, FINSEQ_4:27
.= b by A1, EUCLID:56
.= (f2 /. (i + 1)) `1 by A1, A24, A35, EUCLID:56 ;
hence ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 ) ; :: thesis:

end;

A36: L~ f2 = union {(LSeg p0,p10),(LSeg p10,p1)}

proof

( len f2 = 2 + 1 & 1 + 1 in Seg (len f2) ) by A23, FINSEQ_1:3;
then ( 1 + 1 <= len f2 & LSeg p0,p10 = LSeg f2,1 ) by A24, TOPREAL1:def 5;
then A37: LSeg p0,p10 in { (LSeg f2,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } ;
( 2 + 1 <= len f2 & LSeg p10,p1 = LSeg f2,2 ) by A23, A24, TOPREAL1:def 5;
then LSeg p10,p1 in { (LSeg f2,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } ;
then A38: {(LSeg p0,p10),(LSeg p10,p1)} c= { (LSeg f2,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } by A37, ZFMISC_1:38;
{ (LSeg f2,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } c= {(LSeg p0,p10),(LSeg p10,p1)}

proof

let ax be set ; :: according to TARSKI:def 3 :: thesis:
assume ax in { (LSeg f2,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } ; :: thesis:
then consider i being Element of NAT such that
A39: ( ax = LSeg f2,i & 1 <= i & i + 1 <= len f2 ) ;
i + 1 <= 2 + 1 by A1, A39, FINSEQ_1:62;
then i <= 1 + 1 by XREAL_1:8;
then ( i = 1 or i = 2 ) by A39, NAT_1:9;
then ( ax = LSeg p0,p10 or ax = LSeg p10,p1 ) by A24, A39, TOPREAL1:def 5;
hence ax in {(LSeg p0,p10),(LSeg p10,p1)} by TARSKI:def 2; :: thesis:

end;

hence L~ f2 = union {(LSeg p0,p10),(LSeg p10,p1)} by A38, XBOOLE_0:def 10; :: thesis:

end;

hence L~ f2 = (LSeg p0,p10) \/ (LSeg p10,p1) by ZFMISC_1:93; :: thesis:
L~ f2 = (LSeg p0,p10) \/ (LSeg p10,p1) by A36, ZFMISC_1:93;
then A40: 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, Th39
.= { 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 A1, Th39 ;
rectangle a,b,c,d = ((LSeg p0,p01) \/ (LSeg p01,p1)) \/ ((LSeg p0,p10) \/ (LSeg p10,p1)) by A1, SPPOL_2:def 3;
hence rectangle a,b,c,d = (L~ f1) \/ (L~ f2) by A21, A36, ZFMISC_1:93; :: thesis:

now

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:
then consider x being set such that
A41: ( x in { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) } & x in { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) } ) by XBOOLE_0:3;
A42: ex p being Point of (TOP-REAL 2) st
( p = x & p `1 <= b & p `1 >= a & p `2 = d ) by A41;
ex p2 being Point of (TOP-REAL 2) st
( p2 = x & p2 `1 <= b & p2 `1 >= a & p2 `2 = c ) by A41;
hence contradiction by A1, A42; :: thesis:

end;

then A43: { 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 ) } = {} by XBOOLE_0:def 7;
A44: ( LSeg |[a,c]|,|[a,d]| = { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `1 = a & p3 `2 <= d & p3 `2 >= c ) } & LSeg |[a,d]|,|[b,d]| = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= b & p2 `1 >= a & p2 `2 = d ) } & LSeg |[a,c]|,|[b,c]| = { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 <= b & q1 `1 >= a & q1 `2 = c ) } & LSeg |[b,c]|,|[b,d]| = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = b & q2 `2 <= d & q2 `2 >= c ) } & (LSeg |[a,c]|,|[a,d]|) /\ (LSeg |[a,c]|,|[b,c]|) = {|[a,c]|} & (LSeg |[a,d]|,|[b,d]|) /\ (LSeg |[b,c]|,|[b,d]|) = {|[b,d]|} ) by A1, Th39, Th41, Th43;

now

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:
then consider x being set such that
A45: ( x in { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } & x in { p where p is Point of (TOP-REAL 2) : ( p `1 = b & p `2 <= d & p `2 >= c ) } ) by XBOOLE_0:3;
A46: ex p being Point of (TOP-REAL 2) st
( p = x & p `1 = a & p `2 <= d & p `2 >= c ) by A45;
ex p2 being Point of (TOP-REAL 2) st
( p2 = x & p2 `1 = b & p2 `2 <= d & p2 `2 >= c ) by A45;
hence contradiction by A1, A46; :: thesis:

end;

then A47: { 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 ) } = {} by XBOOLE_0:def 7;
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 A22, A40, 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 A43, XBOOLE_1:23
.= {p0,p1} by A1, A44, A47, ENUMSET1:41 ; :: thesis:
thus ( f1 /. 1 = p0 & f1 /. (len f1) = p1 & f2 /. 1 = p0 & f2 /. (len f2) = p1 ) by A1, A5, A23, FINSEQ_4:27; :: thesis: