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 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: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))} :: according to XBOOLE_0:def 10 :: thesis: {(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 ; :: according to TARSKI:def 3 :: thesis: ( 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 ) } ; :: thesis: 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 ;
per cases then ( j = 1 or j = 2 ) by A8;
suppose j = 1 ; :: thesis: x in {(LSeg (p1,p2)),(LSeg (p2,p3))}
then x = LSeg (p1,p2) by A4, A5, A7, A9, TOPREAL1:def 3;
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 3;
hence x in {(LSeg (p1,p2)),(LSeg (p2,p3))} by TARSKI:def 2; :: thesis: verum
end;
end;
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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))} ; :: thesis: x in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) }
per cases ( x = LSeg (p1,p2) or x = LSeg (p2,p3) ) by A10, TARSKI:def 2;
suppose A11: x = LSeg (p1,p2) ; :: thesis: x in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) }
A12: 1 + 1 <= len f by A2;
x = LSeg (f,1) by A2, A4, A5, A6, A11, TOPREAL1:def 3;
hence x in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } by A12; :: thesis: verum
end;
suppose x = LSeg (p2,p3) ; :: thesis: x in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) }
then x = LSeg (f,2) by A2, A5, A3, TOPREAL1:def 3;
hence x in { (LSeg (f,i)) where i is 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:75; :: thesis: verum