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 by FINSEQ_1:62;
A3: f /. 3 = p3 by A1, FINSEQ_4:27;
A4: f /. 1 = p1 by A1, FINSEQ_4:27;
A5: f /. 2 = p2 by A1, FINSEQ_4:27;
A6: 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
A7: x = LSeg f,j and
A8: 1 <= j and
A9: j + 1 <= len f ;
A10: j <= 2 by A2, A9, XREAL_1:8;

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

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

then x = LSeg p1,p2 by A4, A5, A7, A9, 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, A5, A3, A7, 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 A11: 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 A11, TARSKI:def 2;

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

A13: 1 + 1 <= len f by A2;
x = LSeg f,1 by A2, A4, A5, A6, A12, TOPREAL1:def 5;
hence x in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by A13; :: 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, A5, A3, 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