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

theorem Th1: :: JORDAN17:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for a, p1, p2 being Point of (TOP-REAL n)
for P being Subset of (TOP-REAL n) st a in P & P is_an_arc_of p1,p2 holds
ex f being Function of I[01] ,((TOP-REAL n) | P) ex r being Real st
( f is_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= r & r <= 1 & f . r = a )
proof end;

theorem :: JORDAN17:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Simple_closed_curve holds LE W-min P, E-max P,P
proof end;

theorem :: JORDAN17:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Simple_closed_curve
for a being Point of (TOP-REAL 2) st LE a, E-max P,P holds
a in Upper_Arc P
proof end;

theorem :: JORDAN17:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Simple_closed_curve
for a being Point of (TOP-REAL 2) st LE E-max P,a,P holds
a in Lower_Arc P
proof end;

theorem :: JORDAN17:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Simple_closed_curve
for a being Point of (TOP-REAL 2) st LE a, W-min P,P holds
a in Lower_Arc P
proof end;

theorem Th6: :: JORDAN17:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d being Point of (TOP-REAL 2)
for P being Subset of (TOP-REAL 2) st a <> b & P is_an_arc_of c,d & LE a,b,P,c,d holds
ex e being Point of (TOP-REAL 2) st
( a <> e & b <> e & LE a,e,P,c,d & LE e,b,P,c,d )
proof end;

theorem Th7: :: JORDAN17:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Simple_closed_curve
for a being Point of (TOP-REAL 2) st a in P holds
ex e being Point of (TOP-REAL 2) st
( a <> e & LE a,e,P )
proof end;

theorem Th8: :: JORDAN17:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Simple_closed_curve
for a, b being Point of (TOP-REAL 2) st a <> b & LE a,b,P holds
ex c being Point of (TOP-REAL 2) st
( c <> a & c <> b & LE a,c,P & LE c,b,P )
proof end;

definition
let P be Subset of (TOP-REAL 2);
let a, b, c, d be Point of (TOP-REAL 2);
pred a,b,c,d are_in_this_order_on P means :Def1: :: JORDAN17:def 1
( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) );
end;

:: deftheorem Def1 defines are_in_this_order_on JORDAN17:def 1 :
for P being Subset of (TOP-REAL 2)
for a, b, c, d being Point of (TOP-REAL 2) holds
( a,b,c,d are_in_this_order_on P iff ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) );

theorem :: JORDAN17:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Simple_closed_curve
for a being Point of (TOP-REAL 2) st a in P holds
a,a,a,a are_in_this_order_on P
proof end;

theorem :: JORDAN17:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Simple_closed_curve
for a, b, c, d being Point of (TOP-REAL 2) st a,b,c,d are_in_this_order_on P holds
b,c,d,a are_in_this_order_on P
proof end;

theorem :: JORDAN17:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Simple_closed_curve
for a, b, c, d being Point of (TOP-REAL 2) st a,b,c,d are_in_this_order_on P holds
c,d,a,b are_in_this_order_on P
proof end;

theorem :: JORDAN17:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Simple_closed_curve
for a, b, c, d being Point of (TOP-REAL 2) st a,b,c,d are_in_this_order_on P holds
d,a,b,c are_in_this_order_on P
proof end;

theorem :: JORDAN17:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Simple_closed_curve
for a, b, c, d being Point of (TOP-REAL 2) st a <> b & a,b,c,d are_in_this_order_on P holds
ex e being Point of (TOP-REAL 2) st
( e <> a & e <> b & a,e,b,c are_in_this_order_on P )
proof end;

theorem :: JORDAN17:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Simple_closed_curve
for a, b, c, d being Point of (TOP-REAL 2) st a <> b & a,b,c,d are_in_this_order_on P holds
ex e being Point of (TOP-REAL 2) st
( e <> a & e <> b & a,e,b,d are_in_this_order_on P )
proof end;

theorem :: JORDAN17:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Simple_closed_curve
for b, c, a, d being Point of (TOP-REAL 2) st b <> c & a,b,c,d are_in_this_order_on P holds
ex e being Point of (TOP-REAL 2) st
( e <> b & e <> c & a,b,e,c are_in_this_order_on P )
proof end;

theorem :: JORDAN17:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Simple_closed_curve
for b, c, a, d being Point of (TOP-REAL 2) st b <> c & a,b,c,d are_in_this_order_on P holds
ex e being Point of (TOP-REAL 2) st
( e <> b & e <> c & b,e,c,d are_in_this_order_on P )
proof end;

theorem :: JORDAN17:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Simple_closed_curve
for c, d, a, b being Point of (TOP-REAL 2) st c <> d & a,b,c,d are_in_this_order_on P holds
ex e being Point of (TOP-REAL 2) st
( e <> c & e <> d & a,c,e,d are_in_this_order_on P )
proof end;

theorem :: JORDAN17:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Simple_closed_curve
for c, d, a, b being Point of (TOP-REAL 2) st c <> d & a,b,c,d are_in_this_order_on P holds
ex e being Point of (TOP-REAL 2) st
( e <> c & e <> d & b,c,e,d are_in_this_order_on P )
proof end;

theorem :: JORDAN17:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Simple_closed_curve
for d, a, b, c being Point of (TOP-REAL 2) st d <> a & a,b,c,d are_in_this_order_on P holds
ex e being Point of (TOP-REAL 2) st
( e <> d & e <> a & a,b,d,e are_in_this_order_on P )
proof end;

theorem :: JORDAN17:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Simple_closed_curve
for d, a, b, c being Point of (TOP-REAL 2) st d <> a & a,b,c,d are_in_this_order_on P holds
ex e being Point of (TOP-REAL 2) st
( e <> d & e <> a & a,c,d,e are_in_this_order_on P )
proof end;

theorem :: JORDAN17:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Simple_closed_curve
for a, c, d, b being Point of (TOP-REAL 2) st a <> c & a <> d & b <> d & a,b,c,d are_in_this_order_on P & b,a,c,d are_in_this_order_on P holds
a = b
proof end;

theorem :: JORDAN17:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Simple_closed_curve
for a, b, c, d being Point of (TOP-REAL 2) st a <> b & b <> c & c <> d & a,b,c,d are_in_this_order_on P & c,b,a,d are_in_this_order_on P holds
a = c
proof end;

theorem :: JORDAN17:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Simple_closed_curve
for a, b, c, d being Point of (TOP-REAL 2) st a <> b & a <> c & b <> d & a,b,c,d are_in_this_order_on P & d,b,c,a are_in_this_order_on P holds
a = d
proof end;

theorem :: JORDAN17:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Simple_closed_curve
for a, c, d, b being Point of (TOP-REAL 2) st a <> c & a <> d & b <> d & a,b,c,d are_in_this_order_on P & a,c,b,d are_in_this_order_on P holds
b = c
proof end;

theorem :: JORDAN17:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Simple_closed_curve
for a, b, c, d being Point of (TOP-REAL 2) st a <> b & b <> c & c <> d & a,b,c,d are_in_this_order_on P & a,d,c,b are_in_this_order_on P holds
b = d
proof end;

theorem :: JORDAN17:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Simple_closed_curve
for a, b, c, d being Point of (TOP-REAL 2) st a <> b & a <> c & b <> d & a,b,c,d are_in_this_order_on P & a,b,d,c are_in_this_order_on P holds
c = d
proof end;

theorem :: JORDAN17:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Simple_closed_curve
for a, b, c, d being Point of (TOP-REAL 2) st a in C & b in C & c in C & d in C & not a,b,c,d are_in_this_order_on C & not a,b,d,c are_in_this_order_on C & not a,c,b,d are_in_this_order_on C & not a,c,d,b are_in_this_order_on C & not a,d,b,c are_in_this_order_on C holds
a,d,c,b are_in_this_order_on C
proof end;