let a, b, c, d be real number ; :: 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:56;
A10: p1 `2 = d by A4, EUCLID:56;
A11: p10 `1 = b by A6, EUCLID:56;
A12: p10 `2 = c by A6, EUCLID:56;
A13: p0 `1 = a by A3, EUCLID:56;
A14: p0 `2 = c by A3, EUCLID:56;
A15: len f1 = 1 + 2 by A7, FINSEQ_1:62;
A16: f1 /. 1 = p0 by A7, FINSEQ_4:27;
A17: f1 /. 2 = p01 by A7, FINSEQ_4:27;
A18: f1 /. 3 = p1 by A7, FINSEQ_4:27;
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
A19: p0 <> p01 by A2, A5, A14, EUCLID:56;
p01 <> p1 by A1, A5, A9, EUCLID:56;
hence f1 is one-to-one by A1, A7, A9, A13, A19, FINSEQ_3:104; :: according to TOPREAL1:def 10 :: 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
let i be Nat; :: according to TOPREAL1:def 8 :: 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:8;
then A22: i = 1 by A20, XXREAL_0:1;
reconsider n2 = 1 + 1 as Element of NAT ;
n2 in Seg (len f1) by A15, FINSEQ_1:3;
then A23: LSeg f1,1 = LSeg p0,p01 by A15, A16, A17, TOPREAL1:def 5;
A24: LSeg f1,n2 = LSeg p01,p1 by A15, A17, A18, 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: ( 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) )
proof
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, Th39;
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, Th39;
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:57; :: thesis: verum
end;
assume A31: x = p01 ; :: thesis: x in (LSeg p0,p01) /\ (LSeg p01,p1)
then A32: x in LSeg p0,p01 by RLTOPSP1:69;
x in LSeg p01,p1 by A31, RLTOPSP1:69;
hence x in (LSeg p0,p01) /\ (LSeg p01,p1) by A32, XBOOLE_0:def 4; :: thesis: verum
end;
hence (LSeg f1,i) /\ (LSeg f1,(i + 1)) = {(f1 /. (i + 1))} by A17, A22, A23, A24, TARSKI:def 1; :: thesis: verum
end;
thus f1 is s.n.c. :: thesis: f1 is special
proof
let i, j be Nat; :: according to TOPREAL1:def 9 :: 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
now
per cases ( 1 <= i or not 1 <= i or not i + 1 <= len f1 ) ;
suppose 1 <= i ; :: thesis: (LSeg f1,i) /\ (LSeg f1,j) = {}
then A34: 1 + 1 <= i + 1 by XREAL_1:8;
now
per cases ( ( 1 <= j & j + 1 <= len f1 ) or not 1 <= j or not j + 1 <= len f1 ) ;
case ( not 1 <= j or not j + 1 <= len f1 ) ; :: thesis: (LSeg f1,i) /\ (LSeg f1,j) = {}
then LSeg f1,j = {} by TOPREAL1:def 5;
hence (LSeg f1,i) /\ (LSeg f1,j) = {} ; :: thesis: verum
end;
end;
end;
hence (LSeg f1,i) /\ (LSeg f1,j) = {} ; :: thesis: verum
end;
suppose ( not 1 <= i or not i + 1 <= len f1 ) ; :: thesis: (LSeg f1,i) /\ (LSeg f1,j) = {}
then LSeg f1,i = {} by TOPREAL1:def 5;
hence (LSeg f1,i) /\ (LSeg f1,j) = {} ; :: thesis: verum
end;
end;
end;
hence (LSeg f1,i) /\ (LSeg f1,j) = {} ; :: according to XBOOLE_0:def 7 :: thesis: verum
end;
let i be Nat; :: according to TOPREAL1:def 7 :: 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 )
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:8;
now
per cases ( i = 1 or i = 2 ) by A35, A37, NAT_1:9;
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:27
.= a by A3, EUCLID:56
.= (f1 /. (i + 1)) `1 by A5, A17, A38, EUCLID:56 ;
hence ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 ) ; :: thesis: verum
end;
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:27
.= d by A5, EUCLID:56
.= (f1 /. (i + 1)) `2 by A4, A18, A39, EUCLID:56 ;
hence ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 ) ; :: thesis: verum
end;
end;
end;
hence ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 ) ; :: thesis: verum
end;
A40: 1 + 1 in Seg (len f1) by A15, FINSEQ_1:3;
A41: 1 + 1 <= len f1 by A15;
LSeg p0,p01 = LSeg f1,1 by A15, A16, A17, A40, TOPREAL1:def 5;
then A42: LSeg p0,p01 in { (LSeg f1,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f1 ) } by A41;
LSeg p01,p1 = LSeg f1,2 by A15, A17, A18, TOPREAL1:def 5;
then LSeg p01,p1 in { (LSeg f1,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f1 ) } by A15;
then A43: {(LSeg p0,p01),(LSeg p01,p1)} c= { (LSeg f1,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f1 ) } by A42, 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: ( not a in { (LSeg f1,i) where i is Element of 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 Element of NAT : ( 1 <= i & i + 1 <= len f1 ) } ; :: thesis: a in {(LSeg p0,p01),(LSeg p01,p1)}
then consider i being Element of 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:62;
then i <= 1 + 1 by XREAL_1:8;
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 5;
hence a in {(LSeg p0,p01),(LSeg p01,p1)} by TARSKI:def 2; :: thesis: verum
end;
then L~ f1 = union {(LSeg p0,p01),(LSeg p01,p1)} by A43, XBOOLE_0:def 10;
hence A47: L~ f1 = (LSeg p0,p01) \/ (LSeg p01,p1) by ZFMISC_1:93; :: 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, 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, A4, A5, Th39 ;
A49: len f2 = 1 + 2 by A8, FINSEQ_1:62;
A50: f2 /. 1 = p0 by A8, FINSEQ_4:27;
A51: f2 /. 2 = p10 by A8, FINSEQ_4:27;
A52: f2 /. 3 = p1 by A8, FINSEQ_4:27;
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
thus f2 is one-to-one by A1, A2, A8, A9, A10, A11, A12, A13, FINSEQ_3:104; :: according to TOPREAL1:def 10 :: 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 )
proof
let i be Nat; :: according to TOPREAL1:def 8 :: 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:8;
then A55: i = 1 by A53, XXREAL_0:1;
1 + 1 in Seg (len f2) by A49, FINSEQ_1:3;
then A56: LSeg f2,1 = LSeg p0,p10 by A49, A50, A51, TOPREAL1:def 5;
A57: LSeg f2,(1 + 1) = LSeg p10,p1 by A49, A51, A52, 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: ( 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) )
proof
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, Th39;
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, Th39;
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:57; :: thesis: verum
end;
assume A64: x = p10 ; :: thesis: x in (LSeg p0,p10) /\ (LSeg p10,p1)
then A65: x in LSeg p0,p10 by RLTOPSP1:69;
x in LSeg p10,p1 by A64, RLTOPSP1:69;
hence x in (LSeg p0,p10) /\ (LSeg p10,p1) by A65, XBOOLE_0:def 4; :: thesis: verum
end;
hence (LSeg f2,i) /\ (LSeg f2,(i + 1)) = {(f2 /. (i + 1))} by A51, A55, A56, A57, TARSKI:def 1; :: thesis: verum
end;
thus f2 is s.n.c. :: thesis: f2 is special
proof
let i, j be Nat; :: according to TOPREAL1:def 9 :: 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
now
per cases ( 1 <= i or not 1 <= i or not i + 1 <= len f2 ) ;
suppose 1 <= i ; :: thesis: (LSeg f2,i) /\ (LSeg f2,j) = {}
then A67: 1 + 1 <= i + 1 by XREAL_1:8;
now
per cases ( ( 1 <= j & j + 1 <= len f2 ) or not 1 <= j or not j + 1 <= len f2 ) ;
case ( not 1 <= j or not j + 1 <= len f2 ) ; :: thesis: (LSeg f2,i) /\ (LSeg f2,j) = {}
then LSeg f2,j = {} by TOPREAL1:def 5;
hence (LSeg f2,i) /\ (LSeg f2,j) = {} ; :: thesis: verum
end;
end;
end;
hence (LSeg f2,i) /\ (LSeg f2,j) = {} ; :: thesis: verum
end;
suppose ( not 1 <= i or not i + 1 <= len f2 ) ; :: thesis: (LSeg f2,i) /\ (LSeg f2,j) = {}
then LSeg f2,i = {} by TOPREAL1:def 5;
hence (LSeg f2,i) /\ (LSeg f2,j) = {} ; :: thesis: verum
end;
end;
end;
hence (LSeg f2,i) /\ (LSeg f2,j) = {} ; :: according to XBOOLE_0:def 7 :: thesis: verum
end;
let i be Nat; :: according to TOPREAL1:def 7 :: 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 )
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:8;
per cases ( i = 1 or i = 2 ) by A68, A70, NAT_1:9;
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:27
.= c by A3, EUCLID:56
.= (f2 /. (i + 1)) `2 by A6, A51, A71, EUCLID:56 ;
hence ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 ) ; :: thesis: verum
end;
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:27
.= b by A6, EUCLID:56
.= (f2 /. (i + 1)) `1 by A4, A52, A72, EUCLID:56 ;
hence ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 ) ; :: thesis: verum
end;
end;
end;
A73: 1 + 1 in Seg (len f2) by A49, FINSEQ_1:3;
A74: 1 + 1 <= len f2 by A49;
LSeg p0,p10 = LSeg f2,1 by A49, A50, A51, A73, TOPREAL1:def 5;
then A75: LSeg p0,p10 in { (LSeg f2,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } by A74;
LSeg p10,p1 = LSeg f2,2 by A49, A51, A52, TOPREAL1:def 5;
then LSeg p10,p1 in { (LSeg f2,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } by A49;
then A76: {(LSeg p0,p10),(LSeg p10,p1)} c= { (LSeg f2,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } by A75, 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: ( not ax in { (LSeg f2,i) where i is Element of 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 Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } ; :: thesis: ax in {(LSeg p0,p10),(LSeg p10,p1)}
then consider i being Element of 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:62;
then i <= 1 + 1 by XREAL_1:8;
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 5;
hence ax in {(LSeg p0,p10),(LSeg p10,p1)} by TARSKI:def 2; :: thesis: verum
end;
then A80: L~ f2 = union {(LSeg p0,p10),(LSeg p10,p1)} by A76, XBOOLE_0:def 10;
hence L~ f2 = (LSeg p0,p10) \/ (LSeg p10,p1) by ZFMISC_1:93; :: 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:93;
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, 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 A2, A4, A6, Th39 ;
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:93; :: thesis: ( (L~ f1) /\ (L~ f2) = {p0,p1} & f1 /. 1 = p0 & f1 /. (len f1) = p1 & f2 /. 1 = p0 & f2 /. (len f2) = p1 )
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: contradiction
then consider x being set 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 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 ) } = {} by XBOOLE_0:def 7;
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, Th39;
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, Th39;
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, Th39;
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, Th39;
A90: (LSeg |[a,c]|,|[a,d]|) /\ (LSeg |[a,c]|,|[b,c]|) = {|[a,c]|} by A1, A2, Th41;
A91: (LSeg |[a,d]|,|[b,d]|) /\ (LSeg |[b,c]|,|[b,d]|) = {|[b,d]|} by A1, A2, 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: contradiction
then consider x being set 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 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 ) } = {} 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 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:41 ; :: 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:27; :: thesis: verum