let f1, f2 be FinSequence of ; :: thesis: ( f1,f2 are_in_general_position implies for i, j being Element of 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 Element of 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, Def2;
then A2: L~ f1 misses rng f2 by Def1;
let i, j be Element of 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, Def2;
then A5: L~ f2 misses rng f1 by Def1;

now

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 set 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 REALSET1:14;
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 by A6, A7;
A12: a2 in LSeg (f2 /. j),(f2 /. (j + 1)) by A4, A10, TOPREAL1:def 5;
A13: LSeg f1,i = LSeg (f1 /. i),(f1 /. (i + 1)) by A3, TOPREAL1:def 5;
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 5;
then A15: a1 in (LSeg (f2 /. j),a2) \/ (LSeg a2,(f2 /. (j + 1))) by A12, TOPREAL1:11;
f1 /. i in LSeg (f1 /. i),(f1 /. (i + 1)) by RLTOPSP1:69;
then A16: LSeg a2,(f1 /. i) c= LSeg (f1 /. i),(f1 /. (i + 1)) by A14, TOPREAL1:12;
A17: a1 in (LSeg (f1 /. i),a2) \/ (LSeg a2,(f1 /. (i + 1))) by A9, A13, TOPREAL1:11;
f2 /. j in LSeg (f2 /. j),(f2 /. (j + 1)) by RLTOPSP1:69;
then A18: LSeg a2,(f2 /. j) c= LSeg (f2 /. j),(f2 /. (j + 1)) by A12, TOPREAL1:12;
A19: f2 /. j in rng f2 by A4, Th4;
A20: f1 /. i in rng f1 by A3, Th4;
f2 /. (j + 1) in LSeg (f2 /. j),(f2 /. (j + 1)) by RLTOPSP1:69;
then A21: LSeg a2,(f2 /. (j + 1)) c= LSeg (f2 /. j),(f2 /. (j + 1)) by A12, TOPREAL1:12;
f1 /. (i + 1) in LSeg (f1 /. i),(f1 /. (i + 1)) by RLTOPSP1:69;
then A22: LSeg a2,(f1 /. (i + 1)) c= LSeg (f1 /. i),(f1 /. (i + 1)) by A14, TOPREAL1:12;
A23: f2 /. (j + 1) in rng f2 by A4, Th4;
A24: f1 /. (i + 1) in rng f1 by A3, Th4;

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

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:53;
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

per cases ( f1 /. i in LSeg f2,j or f2 /. j in LSeg f1,i ) by A3, A4, A26, TOPREAL1:def 5;

suppose f1 /. i in LSeg f2,j ; :: thesis: contradiction

then f1 /. i in L~ f2 by SPPOL_2:17;
hence contradiction by A5, A20, XBOOLE_0:3; :: thesis: verum

end;

suppose f2 /. j in LSeg f1,i ; :: thesis: contradiction

then f2 /. j in L~ f1 by SPPOL_2:17;
hence contradiction by A2, A19, 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 in LSeg a2,(f2 /. (j + 1)) or f2 /. (j + 1) in LSeg a2,(f1 /. i) ) by A8, A25, JORDAN4:53;
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

per cases ( f1 /. i in LSeg f2,j or f2 /. (j + 1) in LSeg f1,i ) by A3, A4, A27, TOPREAL1:def 5;

suppose f1 /. i in LSeg f2,j ; :: thesis: contradiction

then f1 /. i in L~ f2 by SPPOL_2:17;
hence contradiction by A5, A20, 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;

suppose A28: a1 in LSeg a2,(f1 /. (i + 1)) ; :: thesis: contradiction

now

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:53;
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

per cases ( f1 /. (i + 1) in LSeg f2,j or f2 /. j in LSeg f1,i ) by A3, A4, A29, TOPREAL1:def 5;

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 in LSeg f1,i ; :: thesis: contradiction

then f2 /. j in L~ f1 by SPPOL_2:17;
hence contradiction by A2, A19, 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:53;
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

per cases ( f1 /. (i + 1) in LSeg f2,j or f2 /. (j + 1) in LSeg f1,i ) by A3, A4, A30, TOPREAL1:def 5;

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