:: JORDAN5C semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: for r being Real st 0 <= r & r <= 1 holds
( 0 <= 1 - r & 1 - r <= 1 )
proof end;

theorem Th1: :: JORDAN5C:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P, Q being Subset of (TOP-REAL 2)
for p1, p2, q1 being Point of (TOP-REAL 2)
for f being Function of I[01] ,((TOP-REAL 2) | P)
for s1 being Real st q1 in P & q1 in Q & f . s1 = q1 & f is_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 0 <= t & t < s1 holds
not f . t in Q ) holds
for g being Function of I[01] ,((TOP-REAL 2) | P)
for s2 being Real st g is_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q
proof end;

definition
let P, Q be Subset of (TOP-REAL 2);
let p1, p2 be Point of (TOP-REAL 2);
assume A1: ( P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 ) ;
func First_Point P,p1,p2,Q -> Point of (TOP-REAL 2) means :Def1: :: JORDAN5C:def 1
( it in P /\ Q & ( for g being Function of I[01] ,((TOP-REAL 2) | P)
for s2 being Real st g is_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = it & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q ) );
existence
ex b1 being Point of (TOP-REAL 2) st
( b1 in P /\ Q & ( for g being Function of I[01] ,((TOP-REAL 2) | P)
for s2 being Real st g is_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q ) )
proof end;
uniqueness
for b1, b2 being Point of (TOP-REAL 2) st b1 in P /\ Q & ( for g being Function of I[01] ,((TOP-REAL 2) | P)
for s2 being Real st g is_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q ) & b2 in P /\ Q & ( for g being Function of I[01] ,((TOP-REAL 2) | P)
for s2 being Real st g is_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b2 & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines First_Point JORDAN5C:def 1 :
for P, Q being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds
for b5 being Point of (TOP-REAL 2) holds
( b5 = First_Point P,p1,p2,Q iff ( b5 in P /\ Q & ( for g being Function of I[01] ,((TOP-REAL 2) | P)
for s2 being Real st g is_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b5 & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q ) ) );

theorem :: JORDAN5C:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P, Q being Subset of (TOP-REAL 2)
for p, p1, p2 being Point of (TOP-REAL 2) st p in P & P is_an_arc_of p1,p2 & Q = {p} holds
First_Point P,p1,p2,Q = p
proof end;

theorem Th3: :: JORDAN5C:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P, Q being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st p1 in Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds
First_Point P,p1,p2,Q = p1
proof end;

theorem Th4: :: JORDAN5C:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P, Q being Subset of (TOP-REAL 2)
for p1, p2, q1 being Point of (TOP-REAL 2)
for f being Function of I[01] ,((TOP-REAL 2) | P)
for s1 being Real st q1 in P & q1 in Q & f . s1 = q1 & f is_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 1 >= t & t > s1 holds
not f . t in Q ) holds
for g being Function of I[01] ,((TOP-REAL 2) | P)
for s2 being Real st g is_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in Q
proof end;

definition
let P, Q be Subset of (TOP-REAL 2);
let p1, p2 be Point of (TOP-REAL 2);
assume A1: ( P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 ) ;
func Last_Point P,p1,p2,Q -> Point of (TOP-REAL 2) means :Def2: :: JORDAN5C:def 2
( it in P /\ Q & ( for g being Function of I[01] ,((TOP-REAL 2) | P)
for s2 being Real st g is_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = it & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in Q ) );
existence
ex b1 being Point of (TOP-REAL 2) st
( b1 in P /\ Q & ( for g being Function of I[01] ,((TOP-REAL 2) | P)
for s2 being Real st g is_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in Q ) )
proof end;
uniqueness
for b1, b2 being Point of (TOP-REAL 2) st b1 in P /\ Q & ( for g being Function of I[01] ,((TOP-REAL 2) | P)
for s2 being Real st g is_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in Q ) & b2 in P /\ Q & ( for g being Function of I[01] ,((TOP-REAL 2) | P)
for s2 being Real st g is_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b2 & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in Q ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Last_Point JORDAN5C:def 2 :
for P, Q being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds
for b5 being Point of (TOP-REAL 2) holds
( b5 = Last_Point P,p1,p2,Q iff ( b5 in P /\ Q & ( for g being Function of I[01] ,((TOP-REAL 2) | P)
for s2 being Real st g is_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b5 & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in Q ) ) );

theorem :: JORDAN5C:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P, Q being Subset of (TOP-REAL 2)
for p, p1, p2 being Point of (TOP-REAL 2) st p in P & P is_an_arc_of p1,p2 & Q = {p} holds
Last_Point P,p1,p2,Q = p
proof end;

theorem Th6: :: JORDAN5C:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P, Q being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st p2 in Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds
Last_Point P,p1,p2,Q = p2
proof end;

theorem Th7: :: JORDAN5C:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P, Q being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P c= Q & P is closed & P is_an_arc_of p1,p2 holds
( First_Point P,p1,p2,Q = p1 & Last_Point P,p1,p2,Q = p2 )
proof end;

definition
let P be Subset of (TOP-REAL 2);
let p1, p2, q1, q2 be Point of (TOP-REAL 2);
pred LE q1,q2,P,p1,p2 means :Def3: :: JORDAN5C:def 3
( q1 in P & q2 in P & ( for g being Function of I[01] ,((TOP-REAL 2) | P)
for s1, s2 being Real st g is_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 holds
s1 <= s2 ) );
end;

:: deftheorem Def3 defines LE JORDAN5C:def 3 :
for P being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds
( LE q1,q2,P,p1,p2 iff ( q1 in P & q2 in P & ( for g being Function of I[01] ,((TOP-REAL 2) | P)
for s1, s2 being Real st g is_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 holds
s1 <= s2 ) ) );

theorem Th8: :: JORDAN5C:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2)
for g being Function of I[01] ,((TOP-REAL 2) | P)
for s1, s2 being Real st P is_an_arc_of p1,p2 & g is_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 & s1 <= s2 holds
LE q1,q2,P,p1,p2
proof end;

theorem Th9: :: JORDAN5C:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2)
for p1, p2, q1 being Point of (TOP-REAL 2) st q1 in P holds
LE q1,q1,P,p1,p2
proof end;

theorem Th10: :: JORDAN5C:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2)
for p1, p2, q1 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P holds
( LE p1,q1,P,p1,p2 & LE q1,p2,P,p1,p2 )
proof end;

theorem :: JORDAN5C:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
LE p1,p2,P,p1,p2
proof end;

theorem Th12: :: JORDAN5C:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 & LE q2,q1,P,p1,p2 holds
q1 = q2
proof end;

theorem Th13: :: JORDAN5C:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2)
for p1, p2, q1, q2, q3 being Point of (TOP-REAL 2) st LE q1,q2,P,p1,p2 & LE q2,q3,P,p1,p2 holds
LE q1,q3,P,p1,p2
proof end;

theorem :: JORDAN5C:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P & q2 in P & q1 <> q2 & not ( LE q1,q2,P,p1,p2 & not LE q2,q1,P,p1,p2 ) holds
( LE q2,q1,P,p1,p2 & not LE q1,q2,P,p1,p2 )
proof end;

theorem Th15: :: JORDAN5C:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2) st f is_S-Seq & (L~ f) /\ Q is closed & q in L~ f & q in Q holds
LE First_Point (L~ f),(f /. 1),(f /. (len f)),Q,q, L~ f,f /. 1,f /. (len f)
proof end;

theorem Th16: :: JORDAN5C:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2) st f is_S-Seq & (L~ f) /\ Q is closed & q in L~ f & q in Q holds
LE q, Last_Point (L~ f),(f /. 1),(f /. (len f)),Q, L~ f,f /. 1,f /. (len f)
proof end;

theorem Th17: :: JORDAN5C:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for q1, q2, p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & LE q1,q2, LSeg p1,p2,p1,p2 holds
LE q1,q2,p1,p2
proof end;

theorem :: JORDAN5C:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P, Q being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & P meets Q & P /\ Q is closed holds
( First_Point P,p1,p2,Q = Last_Point P,p2,p1,Q & Last_Point P,p1,p2,Q = First_Point P,p2,p1,Q )
proof end;

theorem Th19: :: JORDAN5C:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for Q being Subset of (TOP-REAL 2)
for i being Nat st L~ f meets Q & Q is closed & f is_S-Seq & 1 <= i & i + 1 <= len f & First_Point (L~ f),(f /. 1),(f /. (len f)),Q in LSeg f,i holds
First_Point (L~ f),(f /. 1),(f /. (len f)),Q = First_Point (LSeg f,i),(f /. i),(f /. (i + 1)),Q
proof end;

theorem Th20: :: JORDAN5C:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for Q being Subset of (TOP-REAL 2)
for i being Nat st L~ f meets Q & Q is closed & f is_S-Seq & 1 <= i & i + 1 <= len f & Last_Point (L~ f),(f /. 1),(f /. (len f)),Q in LSeg f,i holds
Last_Point (L~ f),(f /. 1),(f /. (len f)),Q = Last_Point (LSeg f,i),(f /. i),(f /. (i + 1)),Q
proof end;

theorem :: JORDAN5C:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for i being Nat st 1 <= i & i + 1 <= len f & f is_S-Seq & First_Point (L~ f),(f /. 1),(f /. (len f)),(LSeg f,i) in LSeg f,i holds
First_Point (L~ f),(f /. 1),(f /. (len f)),(LSeg f,i) = f /. i
proof end;

theorem :: JORDAN5C:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for i being Nat st 1 <= i & i + 1 <= len f & f is_S-Seq & Last_Point (L~ f),(f /. 1),(f /. (len f)),(LSeg f,i) in LSeg f,i holds
Last_Point (L~ f),(f /. 1),(f /. (len f)),(LSeg f,i) = f /. (i + 1)
proof end;

theorem Th23: :: JORDAN5C:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for i being Nat st f is_S-Seq & 1 <= i & i + 1 <= len f holds
LE f /. i,f /. (i + 1), L~ f,f /. 1,f /. (len f)
proof end;

theorem Th24: :: JORDAN5C:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for i, j being Nat st f is_S-Seq & 1 <= i & i <= j & j <= len f holds
LE f /. i,f /. j, L~ f,f /. 1,f /. (len f)
proof end;

Lm2: for f being FinSequence of (TOP-REAL 2)
for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2)
for i being Nat st LSeg f,i meets Q & f is_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg f,i & q in Q holds
LE First_Point (LSeg f,i),(f /. i),(f /. (i + 1)),Q,q,f /. i,f /. (i + 1)
proof end;

Lm3: for f being FinSequence of (TOP-REAL 2)
for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2)
for i being Nat st L~ f meets Q & f is_S-Seq & Q is closed & First_Point (L~ f),(f /. 1),(f /. (len f)),Q in LSeg f,i & 1 <= i & i + 1 <= len f & q in LSeg f,i & q in Q holds
LE First_Point (L~ f),(f /. 1),(f /. (len f)),Q,q,f /. i,f /. (i + 1)
proof end;

Lm4: for f being FinSequence of (TOP-REAL 2)
for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2)
for i being Nat st LSeg f,i meets Q & f is_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg f,i & q in Q holds
LE q, Last_Point (LSeg f,i),(f /. i),(f /. (i + 1)),Q,f /. i,f /. (i + 1)
proof end;

Lm5: for f being FinSequence of (TOP-REAL 2)
for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2)
for i being Nat st L~ f meets Q & f is_S-Seq & Q is closed & Last_Point (L~ f),(f /. 1),(f /. (len f)),Q in LSeg f,i & 1 <= i & i + 1 <= len f & q in LSeg f,i & q in Q holds
LE q, Last_Point (L~ f),(f /. 1),(f /. (len f)),Q,f /. i,f /. (i + 1)
proof end;

theorem Th25: :: JORDAN5C:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for q being Point of (TOP-REAL 2)
for i being Nat st f is_S-Seq & 1 <= i & i + 1 <= len f & q in LSeg f,i holds
LE f /. i,q, L~ f,f /. 1,f /. (len f)
proof end;

theorem Th26: :: JORDAN5C:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for q being Point of (TOP-REAL 2)
for i being Nat st f is_S-Seq & 1 <= i & i + 1 <= len f & q in LSeg f,i holds
LE q,f /. (i + 1), L~ f,f /. 1,f /. (len f)
proof end;

theorem :: JORDAN5C:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2)
for i, j being Nat st L~ f meets Q & f is_S-Seq & Q is closed & First_Point (L~ f),(f /. 1),(f /. (len f)),Q in LSeg f,i & 1 <= i & i + 1 <= len f & q in LSeg f,j & 1 <= j & j + 1 <= len f & q in Q & First_Point (L~ f),(f /. 1),(f /. (len f)),Q <> q holds
( i <= j & ( i = j implies LE First_Point (L~ f),(f /. 1),(f /. (len f)),Q,q,f /. i,f /. (i + 1) ) )
proof end;

theorem :: JORDAN5C:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2)
for i, j being Nat st L~ f meets Q & f is_S-Seq & Q is closed & Last_Point (L~ f),(f /. 1),(f /. (len f)),Q in LSeg f,i & 1 <= i & i + 1 <= len f & q in LSeg f,j & 1 <= j & j + 1 <= len f & q in Q & Last_Point (L~ f),(f /. 1),(f /. (len f)),Q <> q holds
( i >= j & ( i = j implies LE q, Last_Point (L~ f),(f /. 1),(f /. (len f)),Q,f /. i,f /. (i + 1) ) )
proof end;

theorem Th29: :: JORDAN5C:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for q1, q2 being Point of (TOP-REAL 2)
for i being Nat st q1 in LSeg f,i & q2 in LSeg f,i & f is_S-Seq & 1 <= i & i + 1 <= len f & LE q1,q2, L~ f,f /. 1,f /. (len f) holds
LE q1,q2, LSeg f,i,f /. i,f /. (i + 1)
proof end;

theorem :: JORDAN5C:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for q1, q2 being Point of (TOP-REAL 2) st q1 in L~ f & q2 in L~ f & f is_S-Seq & q1 <> q2 holds
( LE q1,q2, L~ f,f /. 1,f /. (len f) iff for i, j being Nat st q1 in LSeg f,i & q2 in LSeg f,j & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f holds
( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) ) )
proof end;