let a, b, c, d be Real; 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); 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); ( 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*>
; ( 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
( 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:52;
p01 <> p1
by A1, A5, A9, EUCLID:52;
hence
f1 is
one-to-one
by A1, A7, A9, A13, A19, FINSEQ_3:95;
TOPREAL1:def 8 ( 2 <= len f1 & f1 is unfolded & f1 is s.n.c. & f1 is special )
thus
len f1 >= 2
by A15;
( f1 is unfolded & f1 is s.n.c. & f1 is special )
thus
f1 is
unfolded
( f1 is s.n.c. & f1 is special )proof
let i be
Nat;
TOPREAL1:def 6 ( 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
;
(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
let x be
object ;
( x in (LSeg (p0,p01)) /\ (LSeg (p01,p1)) iff x = p01 )
thus
(
x in (LSeg (p0,p01)) /\ (LSeg (p01,p1)) implies
x = p01 )
( x = p01 implies x in (LSeg (p0,p01)) /\ (LSeg (p01,p1)) )proof
assume A25:
x in (LSeg (p0,p01)) /\ (LSeg (p01,p1))
;
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;
verum
end;
assume A31:
x = p01
;
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;
verum
end;
hence
(LSeg (f1,i)) /\ (LSeg (f1,(i + 1))) = {(f1 /. (i + 1))}
by A17, A22, A23, A24, TARSKI:def 1;
verum
end;
thus
f1 is
s.n.c.
f1 is special
let i be
Nat;
TOPREAL1:def 5 ( 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
;
( (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;
hence
(
(f1 /. i) `1 = (f1 /. (i + 1)) `1 or
(f1 /. i) `2 = (f1 /. (i + 1)) `2 )
;
verum
end;
A40:
1 + 1 in Seg (len f1)
by A15, FINSEQ_1:1;
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
let a be
object ;
TARSKI:def 3 ( 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 ) }
;
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;
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:75; ( 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
( 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:95;
TOPREAL1:def 8 ( 2 <= len f2 & f2 is unfolded & f2 is s.n.c. & f2 is special )
thus
len f2 >= 2
by A49;
( f2 is unfolded & f2 is s.n.c. & f2 is special )
thus
f2 is
unfolded
( f2 is s.n.c. & f2 is special )proof
let i be
Nat;
TOPREAL1:def 6 ( 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
;
(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
let x be
object ;
( x in (LSeg (p0,p10)) /\ (LSeg (p10,p1)) iff x = p10 )
thus
(
x in (LSeg (p0,p10)) /\ (LSeg (p10,p1)) implies
x = p10 )
( x = p10 implies x in (LSeg (p0,p10)) /\ (LSeg (p10,p1)) )proof
assume A58:
x in (LSeg (p0,p10)) /\ (LSeg (p10,p1))
;
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;
verum
end;
assume A64:
x = p10
;
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;
verum
end;
hence
(LSeg (f2,i)) /\ (LSeg (f2,(i + 1))) = {(f2 /. (i + 1))}
by A51, A55, A56, A57, TARSKI:def 1;
verum
end;
thus
f2 is
s.n.c.
f2 is special
let i be
Nat;
TOPREAL1:def 5 ( 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
;
( (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;
A73:
1 + 1 in Seg (len f2)
by A49, FINSEQ_1:1;
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
let ax be
object ;
TARSKI:def 3 ( 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 ) }
;
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;
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:75; ( 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; ( (L~ f1) /\ (L~ f2) = {p0,p1} & f1 /. 1 = p0 & f1 /. (len f1) = p1 & f2 /. 1 = p0 & f2 /. (len f2) = p1 )
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 ) } = {}
;
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;
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 ) } = {}
;
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
; ( 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; verum