let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: 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); :: thesis: ( f = <*p1,p2,p3*> implies L~ f = (LSeg p1,p2) \/ (LSeg p2,p3) )
set M = { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ;
assume A1: f = <*p1,p2,p3*> ; :: thesis: L~ f = (LSeg p1,p2) \/ (LSeg p2,p3)
then A2: ( len f = 2 + 1 & f /. 1 = p1 & f /. 2 = p2 & f /. 3 = p3 ) by FINSEQ_1:62, FINSEQ_4:27;
A3: 1 + 1 in dom f by A1, Th6;
{ (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } = {(LSeg p1,p2),(LSeg p2,p3)}

proof

thus { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } c= {(LSeg p1,p2),(LSeg p2,p3)} :: according to XBOOLE_0:def 10 :: thesis: {(LSeg p1,p2),(LSeg p2,p3)} c= { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (LSeg f,i) where i is Element of 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 Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; :: thesis: x in {(LSeg p1,p2),(LSeg p2,p3)}
then consider j being Element of NAT such that
A4: ( x = LSeg f,j & 1 <= j & j + 1 <= len f ) ;
A5: ( j <= 2 & j > 0 ) by A2, A4, XREAL_1:8;

per cases ( j = 1 or j = 2 ) by A5, NAT_1:27;

suppose j = 1 ; :: thesis: x in {(LSeg p1,p2),(LSeg p2,p3)}

then x = LSeg p1,p2 by A2, A4, TOPREAL1:def 5;
hence x in {(LSeg p1,p2),(LSeg p2,p3)} by TARSKI:def 2; :: thesis: verum

end;

suppose j = 2 ; :: thesis: x in {(LSeg p1,p2),(LSeg p2,p3)}

then x = LSeg p2,p3 by A2, A4, TOPREAL1:def 5;
hence x in {(LSeg p1,p2),(LSeg p2,p3)} by TARSKI:def 2; :: thesis: verum

end;

end;

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(LSeg p1,p2),(LSeg p2,p3)} or x in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } )
assume A6: x in {(LSeg p1,p2),(LSeg p2,p3)} ; :: thesis: x in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) }

per cases ( x = LSeg p1,p2 or x = LSeg p2,p3 ) by A6, TARSKI:def 2;

suppose x = LSeg p1,p2 ; :: thesis: x in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) }

then A7: x = LSeg f,1 by A2, A3, TOPREAL1:def 5;
1 + 1 <= len f by A2;
hence x in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by A7; :: thesis: verum

end;

suppose x = LSeg p2,p3 ; :: thesis: x in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) }

then x = LSeg f,2 by A2, TOPREAL1:def 5;
hence x in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by A2; :: thesis: verum

end;

end;

end;

hence L~ f = (LSeg p1,p2) \/ (LSeg p2,p3) by ZFMISC_1:93; :: thesis: verum