:: AFF_2 semantic presentation

definition

let AP be AffinPlane;
attr AP is satisfying_PPAP means :Def1: :: AFF_2:def 1
for M, N being Subset of AP
for a, b, c, a', b', c' being Element of AP st M is_line & N is_line & a in M & b in M & c in M & a' in N & b' in N & c' in N & a,b' // b,a' & b,c' // c,b' holds
a,c' // c,a';

end;

:: deftheorem Def1 defines satisfying_PPAP AFF_2:def 1 :

notation

let AP be AffinPlane;
synonym AP satisfies_PPAP for satisfying_PPAP AP;

end;

definition

let AP be AffinSpace;
attr AP is Pappian means :Def2: :: AFF_2:def 2
for M, N being Subset of AP
for o, a, b, c, a', b', c' being Element of AP st M is_line & N is_line & M <> N & o in M & o in N & o <> a & o <> a' & o <> b & o <> b' & o <> c & o <> c' & a in M & b in M & c in M & a' in N & b' in N & c' in N & a,b' // b,a' & b,c' // c,b' holds
a,c' // c,a';

end;

:: deftheorem Def2 defines Pappian AFF_2:def 2 :

notation

let AP be AffinSpace;
synonym AP satisfies_PAP for Pappian AP;

end;

definition

let AP be AffinPlane;
attr AP is satisfying_PAP_1 means :Def3: :: AFF_2:def 3
for M, N being Subset of AP
for o, a, b, c, a', b', c' being Element of AP st M is_line & N is_line & M <> N & o in M & o in N & o <> a & o <> a' & o <> b & o <> b' & o <> c & o <> c' & a in M & b in M & c in M & b' in N & c' in N & a,b' // b,a' & b,c' // c,b' & a,c' // c,a' & b <> c holds
a' in N;

end;

:: deftheorem Def3 defines satisfying_PAP_1 AFF_2:def 3 :

notation

let AP be AffinPlane;
synonym AP satisfies_PAP_1 for satisfying_PAP_1 AP;

end;

definition

let AP be AffinSpace;
attr AP is Desarguesian means :Def4: :: AFF_2:def 4
for A, P, C being Subset of AP
for o, a, b, c, a', b', c' being Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is_line & P is_line & C is_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c';

end;

:: deftheorem Def4 defines Desarguesian AFF_2:def 4 :

notation

let AP be AffinSpace;
synonym AP satisfies_DES for Desarguesian AP;

end;

definition

let AP be AffinPlane;
attr AP is satisfying_DES_1 means :Def5: :: AFF_2:def 5
for A, P, C being Subset of AP
for o, a, b, c, a', b', c' being Element of AP st o in A & o in P & o <> a & o <> b & o <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is_line & P is_line & C is_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' & b,c // b',c' & not LIN a,b,c & c <> c' holds
o in C;

end;

:: deftheorem Def5 defines satisfying_DES_1 AFF_2:def 5 :

notation

let AP be AffinPlane;
synonym AP satisfies_DES_1 for satisfying_DES_1 AP;

end;

definition

let AP be AffinPlane;
attr AP is satisfying_DES_2 means :: AFF_2:def 6
for A, P, C being Subset of AP
for o, a, b, c, a', b', c' being Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a' in A & b in P & b' in P & c in C & A is_line & P is_line & C is_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' & b,c // b',c' holds
c' in C;

end;

:: deftheorem defines satisfying_DES_2 AFF_2:def 6 :

notation

let AP be AffinPlane;
synonym AP satisfies_DES_2 for satisfying_DES_2 AP;

end;

definition

let AP be AffinSpace;
attr AP is Moufangian means :Def7: :: AFF_2:def 7
for K being Subset of AP
for o, a, b, c, a', b', c' being Element of AP st K is_line & o in K & c in K & c' in K & not a in K & o <> c & a <> b & LIN o,a,a' & LIN o,b,b' & a,b // a',b' & a,c // a',c' & a,b // K holds
b,c // b',c';

end;

:: deftheorem Def7 defines Moufangian AFF_2:def 7 :

notation

let AP be AffinSpace;
synonym AP satisfies_TDES for Moufangian AP;

end;

definition

let AP be AffinPlane;
attr AP is satisfying_TDES_1 means :Def8: :: AFF_2:def 8
for K being Subset of AP
for o, a, b, c, a', b', c' being Element of AP st K is_line & o in K & c in K & c' in K & not a in K & o <> c & a <> b & LIN o,a,a' & a,b // a',b' & b,c // b',c' & a,c // a',c' & a,b // K holds
LIN o,b,b';

end;

:: deftheorem Def8 defines satisfying_TDES_1 AFF_2:def 8 :

notation

let AP be AffinPlane;
synonym AP satisfies_TDES_1 for satisfying_TDES_1 AP;

end;

definition

let AP be AffinPlane;
attr AP is satisfying_TDES_2 means :Def9: :: AFF_2:def 9
for K being Subset of AP
for o, a, b, c, a', b', c' being Element of AP st K is_line & o in K & c in K & c' in K & not a in K & o <> c & a <> b & LIN o,a,a' & LIN o,b,b' & b,c // b',c' & a,c // a',c' & a,b // K holds
a,b // a',b';

end;

:: deftheorem Def9 defines satisfying_TDES_2 AFF_2:def 9 :

notation

let AP be AffinPlane;
synonym AP satisfies_TDES_2 for satisfying_TDES_2 AP;

end;

definition

let AP be AffinPlane;
attr AP is satisfying_TDES_3 means :Def10: :: AFF_2:def 10
for K being Subset of AP
for o, a, b, c, a', b', c' being Element of AP st K is_line & o in K & c in K & not a in K & o <> c & a <> b & LIN o,a,a' & LIN o,b,b' & a,b // a',b' & a,c // a',c' & b,c // b',c' & a,b // K holds
c' in K;

end;

:: deftheorem Def10 defines satisfying_TDES_3 AFF_2:def 10 :

notation

let AP be AffinPlane;
synonym AP satisfies_TDES_3 for satisfying_TDES_3 AP;

end;

definition

let AP be AffinSpace;
attr AP is translational means :Def11: :: AFF_2:def 11
for A, P, C being Subset of AP
for a, b, c, a', b', c' being Element of AP st A // P & A // C & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is_line & P is_line & C is_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c';

end;

:: deftheorem Def11 defines translational AFF_2:def 11 :

notation

let AP be AffinSpace;
synonym AP satisfies_des for translational AP;

end;

definition

let AP be AffinPlane;
attr AP is satisfying_des_1 means :Def12: :: AFF_2:def 12
for A, P, C being Subset of AP
for a, b, c, a', b', c' being Element of AP st A // P & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is_line & P is_line & C is_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' & b,c // b',c' & not LIN a,b,c & c <> c' holds
A // C;

end;

:: deftheorem Def12 defines satisfying_des_1 AFF_2:def 12 :

notation

let AP be AffinPlane;
synonym AP satisfies_des_1 for satisfying_des_1 AP;

end;

definition

let AP be AffinSpace;
attr AP is satisfying_pap means :Def13: :: AFF_2:def 13
for M, N being Subset of AP
for a, b, c, a', b', c' being Element of AP st M is_line & N is_line & a in M & b in M & c in M & M // N & M <> N & a' in N & b' in N & c' in N & a,b' // b,a' & b,c' // c,b' holds
a,c' // c,a';

end;

:: deftheorem Def13 defines satisfying_pap AFF_2:def 13 :

notation

let AP be AffinSpace;
synonym AP satisfies_pap for satisfying_pap AP;

end;

definition

let AP be AffinPlane;
attr AP is satisfying_pap_1 means :Def14: :: AFF_2:def 14
for M, N being Subset of AP
for a, b, c, a', b', c' being Element of AP st M is_line & N is_line & a in M & b in M & c in M & M // N & M <> N & a' in N & b' in N & a,b' // b,a' & b,c' // c,b' & a,c' // c,a' & a' <> b' holds
c' in N;

end;