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

definition
let AP be AffinPlane;
attr AP is satisfying_DES1 means :Def1: :: AFF_3:def 1
for A, P, C being Subset of AP
for o, a, a', b, b', c, c', p, q being Element of AP st A is_line & P is_line & C is_line & P <> A & P <> C & A <> C & o in A & a in A & a' in A & o in P & b in P & b' in P & o in C & c in C & c' in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b',a',c' & a <> a' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // a',c' holds
a,c // p,q;
end;

:: deftheorem Def1 defines satisfying_DES1 AFF_3:def 1 :
for AP being AffinPlane holds
( AP is satisfying_DES1 iff for A, P, C being Subset of AP
for o, a, a', b, b', c, c', p, q being Element of AP st A is_line & P is_line & C is_line & P <> A & P <> C & A <> C & o in A & a in A & a' in A & o in P & b in P & b' in P & o in C & c in C & c' in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b',a',c' & a <> a' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // a',c' holds
a,c // p,q );

notation
let AP be AffinPlane;
synonym AP satisfies_DES1 for satisfying_DES1 AP;
end;

definition
let AP be AffinPlane;
attr AP is satisfying_DES1_1 means :Def2: :: AFF_3:def 2
for A, P, C being Subset of AP
for o, a, a', b, b', c, c', p, q being Element of AP st A is_line & P is_line & C is_line & P <> A & P <> C & A <> C & o in A & a in A & a' in A & o in P & b in P & b' in P & o in C & c in C & c' in C & o <> a & o <> b & o <> c & p <> q & c <> q & not LIN b,a,c & not LIN b',a',c' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // p,q holds
a,c // a',c';
end;

:: deftheorem Def2 defines satisfying_DES1_1 AFF_3:def 2 :
for AP being AffinPlane holds
( AP is satisfying_DES1_1 iff for A, P, C being Subset of AP
for o, a, a', b, b', c, c', p, q being Element of AP st A is_line & P is_line & C is_line & P <> A & P <> C & A <> C & o in A & a in A & a' in A & o in P & b in P & b' in P & o in C & c in C & c' in C & o <> a & o <> b & o <> c & p <> q & c <> q & not LIN b,a,c & not LIN b',a',c' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // p,q holds
a,c // a',c' );

notation
let AP be AffinPlane;
synonym AP satisfies_DES1_1 for satisfying_DES1_1 AP;
end;

definition
let AP be AffinPlane;
attr AP is satisfying_DES1_2 means :Def3: :: AFF_3:def 3
for A, P, C being Subset of AP
for o, a, a', b, b', c, c', p, q being Element of AP st A is_line & P is_line & C is_line & P <> A & P <> C & A <> C & o in A & a in A & a' in A & o in P & b in P & b' in P & c in C & c' in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b',a',c' & c <> c' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // a',c' & a,c // p,q holds
o in C;
end;

:: deftheorem Def3 defines satisfying_DES1_2 AFF_3:def 3 :
for AP being AffinPlane holds
( AP is satisfying_DES1_2 iff for A, P, C being Subset of AP
for o, a, a', b, b', c, c', p, q being Element of AP st A is_line & P is_line & C is_line & P <> A & P <> C & A <> C & o in A & a in A & a' in A & o in P & b in P & b' in P & c in C & c' in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b',a',c' & c <> c' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // a',c' & a,c // p,q holds
o in C );

notation
let AP be AffinPlane;
synonym AP satisfies_DES1_2 for satisfying_DES1_2 AP;
end;

definition
let AP be AffinPlane;
attr AP is satisfying_DES1_3 means :Def4: :: AFF_3:def 4
for A, P, C being Subset of AP
for o, a, a', b, b', c, c', p, q being Element of AP st A is_line & P is_line & C is_line & P <> A & P <> C & A <> C & o in A & a in A & a' in A & b in P & b' in P & o in C & c in C & c' in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b',a',c' & b <> b' & a <> a' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // a',c' & a,c // p,q holds
o in P;
end;

:: deftheorem Def4 defines satisfying_DES1_3 AFF_3:def 4 :
for AP being AffinPlane holds
( AP is satisfying_DES1_3 iff for A, P, C being Subset of AP
for o, a, a', b, b', c, c', p, q being Element of AP st A is_line & P is_line & C is_line & P <> A & P <> C & A <> C & o in A & a in A & a' in A & b in P & b' in P & o in C & c in C & c' in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b',a',c' & b <> b' & a <> a' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // a',c' & a,c // p,q holds
o in P );

notation
let AP be AffinPlane;
synonym AP satisfies_DES1_3 for satisfying_DES1_3 AP;
end;

definition
let AP be AffinPlane;
attr AP is satisfying_DES2 means :Def5: :: AFF_3:def 5
for A, P, C being Subset of AP
for a, a', b, b', c, c', p, q being Element of AP st A is_line & P is_line & C is_line & A <> P & A <> C & P <> C & a in A & a' in A & b in P & b' in P & c in C & c' in C & A // P & A // C & not LIN b,a,c & not LIN b',a',c' & p <> q & a <> a' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // a',c' holds
a,c // p,q;
end;

:: deftheorem Def5 defines satisfying_DES2 AFF_3:def 5 :
for AP being AffinPlane holds
( AP is satisfying_DES2 iff for A, P, C being Subset of AP
for a, a', b, b', c, c', p, q being Element of AP st A is_line & P is_line & C is_line & A <> P & A <> C & P <> C & a in A & a' in A & b in P & b' in P & c in C & c' in C & A // P & A // C & not LIN b,a,c & not LIN b',a',c' & p <> q & a <> a' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // a',c' holds
a,c // p,q );

notation
let AP be AffinPlane;
synonym AP satisfies_DES2 for satisfying_DES2 AP;
end;

definition
let AP be AffinPlane;
attr AP is satisfying_DES2_1 means :Def6: :: AFF_3:def 6
for A, P, C being Subset of AP
for a, a', b, b', c, c', p, q being Element of AP st A is_line & P is_line & C is_line & A <> P & A <> C & P <> C & a in A & a' in A & b in P & b' in P & c in C & c' in C & A // P & A // C & not LIN b,a,c & not LIN b',a',c' & p <> q & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // p,q holds
a,c // a',c';
end;

:: deftheorem Def6 defines satisfying_DES2_1 AFF_3:def 6 :
for AP being AffinPlane holds
( AP is satisfying_DES2_1 iff for A, P, C being Subset of AP
for a, a', b, b', c, c', p, q being Element of AP st A is_line & P is_line & C is_line & A <> P & A <> C & P <> C & a in A & a' in A & b in P & b' in P & c in C & c' in C & A // P & A // C & not LIN b,a,c & not LIN b',a',c' & p <> q & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // p,q holds
a,c // a',c' );

notation
let AP be AffinPlane;
synonym AP satisfies_DES2_1 for satisfying_DES2_1 AP;
end;

definition
let AP be AffinPlane;
attr AP is satisfying_DES2_2 means :Def7: :: AFF_3:def 7
for A, P, C being Subset of AP
for a, a', b, b', c, c', p, q being Element of AP st A is_line & P is_line & C is_line & A <> P & A <> C & P <> C & a in A & a' in A & b in P & b' in P & c in C & c' in C & A // C & not LIN b,a,c & not LIN b',a',c' & p <> q & a <> a' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // a',c' & a,c // p,q holds
A // P;
end;

:: deftheorem Def7 defines satisfying_DES2_2 AFF_3:def 7 :
for AP being AffinPlane holds
( AP is satisfying_DES2_2 iff for A, P, C being Subset of AP
for a, a', b, b', c, c', p, q being Element of AP st A is_line & P is_line & C is_line & A <> P & A <> C & P <> C & a in A & a' in A & b in P & b' in P & c in C & c' in C & A // C & not LIN b,a,c & not LIN b',a',c' & p <> q & a <> a' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // a',c' & a,c // p,q holds
A // P );

notation
let AP be AffinPlane;
synonym AP satisfies_DES2_2 for satisfying_DES2_2 AP;
end;

definition
let AP be AffinPlane;
attr AP is satisfying_DES2_3 means :Def8: :: AFF_3:def 8
for A, P, C being Subset of AP
for a, a', b, b', c, c', p, q being Element of AP st A is_line & P is_line & C is_line & A <> P & A <> C & P <> C & a in A & a' in A & b in P & b' in P & c in C & c' in C & A // P & not LIN b,a,c & not LIN b',a',c' & p <> q & c <> c' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // a',c' & a,c // p,q holds
A // C;
end;

:: deftheorem Def8 defines satisfying_DES2_3 AFF_3:def 8 :
for AP being AffinPlane holds
( AP is satisfying_DES2_3 iff for A, P, C being Subset of AP
for a, a', b, b', c, c', p, q being Element of AP st A is_line & P is_line & C is_line & A <> P & A <> C & P <> C & a in A & a' in A & b in P & b' in P & c in C & c' in C & A // P & not LIN b,a,c & not LIN b',a',c' & p <> q & c <> c' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // a',c' & a,c // p,q holds
A // C );

notation
let AP be AffinPlane;
synonym AP satisfies_DES2_3 for satisfying_DES2_3 AP;
end;

theorem :: AFF_3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: AFF_3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: AFF_3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: AFF_3:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: AFF_3:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: AFF_3:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: AFF_3:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: AFF_3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: AFF_3:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AP being AffinPlane st AP satisfies_DES1 holds
AP satisfies_DES1_1
proof end;

theorem :: AFF_3:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AP being AffinPlane st AP satisfies_DES1_1 holds
AP satisfies_DES1
proof end;

theorem :: AFF_3:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AP being AffinPlane st AP satisfies_DES holds
AP satisfies_DES1
proof end;

theorem :: AFF_3:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AP being AffinPlane st AP satisfies_DES holds
AP satisfies_DES1_2
proof end;

theorem :: AFF_3:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AP being AffinPlane st AP satisfies_DES1_2 holds
AP satisfies_DES1_3
proof end;

theorem :: AFF_3:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AP being AffinPlane st AP satisfies_DES1_2 holds
AP satisfies_DES
proof end;

theorem :: AFF_3:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AP being AffinPlane st AP satisfies_DES2_1 holds
AP satisfies_DES2
proof end;

theorem :: AFF_3:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AP being AffinPlane holds
( AP satisfies_DES2_1 iff AP satisfies_DES2_3 )
proof end;

theorem :: AFF_3:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AP being AffinPlane holds
( AP satisfies_DES2 iff AP satisfies_DES2_2 )
proof end;

theorem :: AFF_3:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AP being AffinPlane st AP satisfies_DES1_3 holds
AP satisfies_DES2_1
proof end;