let f1, f2 be FinSequence of (TOP-REAL 2); :: thesis: ( f1,f2 are_in_general_position implies for i, j being Nat st 1 <= i & i + 1 <= len f1 & 1 <= j & j + 1 <= len f2 holds
(LSeg (f1,i)) /\ (LSeg (f2,j)) is trivial )
assume A1: f1,f2 are_in_general_position ; :: thesis: for i, j being Nat st 1 <= i & i + 1 <= len f1 & 1 <= j & j + 1 <= len f2 holds
(LSeg (f1,i)) /\ (LSeg (f2,j)) is trivial
f1 is_in_general_position_wrt f2 by A1;
then A2: L~ f1 misses rng f2 ;
let i, j be Nat; :: thesis: ( 1 <= i & i + 1 <= len f1 & 1 <= j & j + 1 <= len f2 implies (LSeg (f1,i)) /\ (LSeg (f2,j)) is trivial )
assume that
A3: ( 1 <= i & i + 1 <= len f1 ) and
A4: ( 1 <= j & j + 1 <= len f2 ) ; :: thesis: (LSeg (f1,i)) /\ (LSeg (f2,j)) is trivial
f2 is_in_general_position_wrt f1 by A1;
then A5: L~ f2 misses rng f1 ;
now :: thesis: (LSeg (f1,i)) /\ (LSeg (f2,j)) is trivial
set B1 = LSeg ((f1 /. i),(f1 /. (i + 1)));
set B2 = LSeg ((f2 /. j),(f2 /. (j + 1)));
set A1 = LSeg (f1,i);
set A2 = LSeg (f2,j);
set A = (LSeg (f1,i)) /\ (LSeg (f2,j));
assume not (LSeg (f1,i)) /\ (LSeg (f2,j)) is trivial ; :: thesis: contradiction
then consider a1, a2 being object such that
A6: a1 in (LSeg (f1,i)) /\ (LSeg (f2,j)) and
A7: a2 in (LSeg (f1,i)) /\ (LSeg (f2,j)) and
A8: a1 <> a2 by ZFMISC_1:def 10;
A9: ( a1 in LSeg (f1,i) & a2 in LSeg (f1,i) ) by A6, A7, XBOOLE_0:def 4;
A10: a2 in LSeg (f2,j) by A7, XBOOLE_0:def 4;
A11: a1 in LSeg (f2,j) by A6, XBOOLE_0:def 4;
reconsider a1 = a1, a2 = a2 as Point of (TOP-REAL 2) by A6, A7;
A12: a2 in LSeg ((f2 /. j),(f2 /. (j + 1))) by A4, A10, TOPREAL1:def 3;
A13: LSeg (f1,i) = LSeg ((f1 /. i),(f1 /. (i + 1))) by A3, TOPREAL1:def 3;
then A14: a2 in LSeg ((f1 /. i),(f1 /. (i + 1))) by A7, XBOOLE_0:def 4;
a1 in LSeg ((f2 /. j),(f2 /. (j + 1))) by A4, A11, TOPREAL1:def 3;
then A15: a1 in (LSeg ((f2 /. j),a2)) \/ (LSeg (a2,(f2 /. (j + 1)))) by A12, TOPREAL1:5;
f1 /. i in LSeg ((f1 /. i),(f1 /. (i + 1))) by RLTOPSP1:68;
then A16: LSeg (a2,(f1 /. i)) c= LSeg ((f1 /. i),(f1 /. (i + 1))) by A14, TOPREAL1:6;
A17: a1 in (LSeg ((f1 /. i),a2)) \/ (LSeg (a2,(f1 /. (i + 1)))) by A9, A13, TOPREAL1:5;
f2 /. j in LSeg ((f2 /. j),(f2 /. (j + 1))) by RLTOPSP1:68;
then A18: LSeg (a2,(f2 /. j)) c= LSeg ((f2 /. j),(f2 /. (j + 1))) by A12, TOPREAL1:6;
A19: f2 /. j in rng f2 by A4, Th3;
A20: f1 /. i in rng f1 by A3, Th3;
f2 /. (j + 1) in LSeg ((f2 /. j),(f2 /. (j + 1))) by RLTOPSP1:68;
then A21: LSeg (a2,(f2 /. (j + 1))) c= LSeg ((f2 /. j),(f2 /. (j + 1))) by A12, TOPREAL1:6;
f1 /. (i + 1) in LSeg ((f1 /. i),(f1 /. (i + 1))) by RLTOPSP1:68;
then A22: LSeg (a2,(f1 /. (i + 1))) c= LSeg ((f1 /. i),(f1 /. (i + 1))) by A14, TOPREAL1:6;
A23: f2 /. (j + 1) in rng f2 by A4, Th3;
A24: f1 /. (i + 1) in rng f1 by A3, Th3;
per cases ( a1 in LSeg ((f1 /. i),a2) or a1 in LSeg (a2,(f1 /. (i + 1))) ) by A17, XBOOLE_0:def 3;
suppose A25: a1 in LSeg ((f1 /. i),a2) ; :: thesis: contradiction
now :: thesis: contradiction
per cases ( a1 in LSeg ((f2 /. j),a2) or a1 in LSeg (a2,(f2 /. (j + 1))) ) by A15, XBOOLE_0:def 3;
suppose a1 in LSeg ((f2 /. j),a2) ; :: thesis: contradiction
then ( f1 /. i in LSeg (a2,(f2 /. j)) or f2 /. j in LSeg (a2,(f1 /. i)) ) by A8, A25, JORDAN4:41;
then A26: ( f1 /. i in LSeg ((f2 /. j),(f2 /. (j + 1))) or f2 /. j in LSeg ((f1 /. i),(f1 /. (i + 1))) ) by A18, A16;
now :: thesis: contradiction
end;
hence contradiction ; :: thesis: verum
end;
suppose a1 in LSeg (a2,(f2 /. (j + 1))) ; :: thesis: contradiction
then ( f1 /. i in LSeg (a2,(f2 /. (j + 1))) or f2 /. (j + 1) in LSeg (a2,(f1 /. i)) ) by A8, A25, JORDAN4:41;
then A27: ( f1 /. i in LSeg ((f2 /. j),(f2 /. (j + 1))) or f2 /. (j + 1) in LSeg ((f1 /. i),(f1 /. (i + 1))) ) by A16, A21;
now :: thesis: contradiction
per cases ( f1 /. i in LSeg (f2,j) or f2 /. (j + 1) in LSeg (f1,i) ) by A3, A4, A27, TOPREAL1:def 3;
suppose f2 /. (j + 1) in LSeg (f1,i) ; :: thesis: contradiction
then f2 /. (j + 1) in L~ f1 by SPPOL_2:17;
hence contradiction by A2, A23, XBOOLE_0:3; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
suppose A28: a1 in LSeg (a2,(f1 /. (i + 1))) ; :: thesis: contradiction
now :: thesis: contradiction
per cases ( a1 in LSeg ((f2 /. j),a2) or a1 in LSeg (a2,(f2 /. (j + 1))) ) by A15, XBOOLE_0:def 3;
suppose a1 in LSeg ((f2 /. j),a2) ; :: thesis: contradiction
then ( f1 /. (i + 1) in LSeg (a2,(f2 /. j)) or f2 /. j in LSeg (a2,(f1 /. (i + 1))) ) by A8, A28, JORDAN4:41;
then A29: ( f1 /. (i + 1) in LSeg ((f2 /. j),(f2 /. (j + 1))) or f2 /. j in LSeg ((f1 /. i),(f1 /. (i + 1))) ) by A18, A22;
now :: thesis: contradiction
per cases ( f1 /. (i + 1) in LSeg (f2,j) or f2 /. j in LSeg (f1,i) ) by A3, A4, A29, TOPREAL1:def 3;
suppose f1 /. (i + 1) in LSeg (f2,j) ; :: thesis: contradiction
then f1 /. (i + 1) in L~ f2 by SPPOL_2:17;
hence contradiction by A5, A24, XBOOLE_0:3; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
suppose a1 in LSeg (a2,(f2 /. (j + 1))) ; :: thesis: contradiction
then ( f1 /. (i + 1) in LSeg (a2,(f2 /. (j + 1))) or f2 /. (j + 1) in LSeg (a2,(f1 /. (i + 1))) ) by A8, A28, JORDAN4:41;
then A30: ( f1 /. (i + 1) in LSeg ((f2 /. j),(f2 /. (j + 1))) or f2 /. (j + 1) in LSeg ((f1 /. i),(f1 /. (i + 1))) ) by A22, A21;
now :: thesis: contradiction
per cases ( f1 /. (i + 1) in LSeg (f2,j) or f2 /. (j + 1) in LSeg (f1,i) ) by A3, A4, A30, TOPREAL1:def 3;
suppose f1 /. (i + 1) in LSeg (f2,j) ; :: thesis: contradiction
then f1 /. (i + 1) in L~ f2 by SPPOL_2:17;
hence contradiction by A5, A24, XBOOLE_0:3; :: thesis: verum
end;
suppose f2 /. (j + 1) in LSeg (f1,i) ; :: thesis: contradiction
then f2 /. (j + 1) in L~ f1 by SPPOL_2:17;
hence contradiction by A2, A23, XBOOLE_0:3; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;
end;
hence (LSeg (f1,i)) /\ (LSeg (f2,j)) is trivial ; :: thesis: verum