let p1, p2, p3 be Point of (TOP-REAL 2); for f being FinSequence of (TOP-REAL 2) st f = <*p1,p2,p3*> holds
L~ f = (LSeg (p1,p2)) \/ (LSeg (p2,p3))
let f be FinSequence of (TOP-REAL 2); ( f = <*p1,p2,p3*> implies L~ f = (LSeg (p1,p2)) \/ (LSeg (p2,p3)) )
set M = { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } ;
assume A1:
f = <*p1,p2,p3*>
; L~ f = (LSeg (p1,p2)) \/ (LSeg (p2,p3))
then A2:
len f = 2 + 1
by FINSEQ_1:45;
A3:
f /. 3 = p3
by A1, FINSEQ_4:18;
A4:
f /. 1 = p1
by A1, FINSEQ_4:18;
A5:
f /. 2 = p2
by A1, FINSEQ_4:18;
A6:
1 + 1 in dom f
by A1, Th1;
{ (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } = {(LSeg (p1,p2)),(LSeg (p2,p3))}
proof
thus
{ (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } c= {(LSeg (p1,p2)),(LSeg (p2,p3))}
XBOOLE_0:def 10 {(LSeg (p1,p2)),(LSeg (p2,p3))} c= { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } proof
let x be
object ;
TARSKI:def 3 ( not x in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } or x in {(LSeg (p1,p2)),(LSeg (p2,p3))} )
assume
x in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) }
;
x in {(LSeg (p1,p2)),(LSeg (p2,p3))}
then consider j being
Nat such that A7:
x = LSeg (
f,
j)
and A8:
1
<= j
and A9:
j + 1
<= len f
;
j <= 2
by A2, A9, XREAL_1:6;
then
not not
j = 0 & ... & not
j = 2
;
end;
let x be
object ;
TARSKI:def 3 ( not x in {(LSeg (p1,p2)),(LSeg (p2,p3))} or x in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } )
assume A10:
x in {(LSeg (p1,p2)),(LSeg (p2,p3))}
;
x in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) }
end;
hence
L~ f = (LSeg (p1,p2)) \/ (LSeg (p2,p3))
by ZFMISC_1:75; verum