begin
definition
let AP be
AffinPlane;
attr AP is
satisfying_PPAP means :
Def1:
for
M,
N being
Subset of
AP for
a,
b,
c,
a9,
b9,
c9 being
Element of
AP st
M is
being_line &
N is
being_line &
a in M &
b in M &
c in M &
a9 in N &
b9 in N &
c9 in N &
a,
b9 // b,
a9 &
b,
c9 // c,
b9 holds
a,
c9 // c,
a9;
end;
::
deftheorem Def1 defines
satisfying_PPAP AFF_2:def 1 :
for AP being AffinPlane holds
( AP is satisfying_PPAP iff for M, N being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9 );
definition
let AP be
AffinSpace;
attr AP is
Pappian means :
Def2:
for
M,
N being
Subset of
AP for
o,
a,
b,
c,
a9,
b9,
c9 being
Element of
AP st
M is
being_line &
N is
being_line &
M <> N &
o in M &
o in N &
o <> a &
o <> a9 &
o <> b &
o <> b9 &
o <> c &
o <> c9 &
a in M &
b in M &
c in M &
a9 in N &
b9 in N &
c9 in N &
a,
b9 // b,
a9 &
b,
c9 // c,
b9 holds
a,
c9 // c,
a9;
end;
::
deftheorem Def2 defines
Pappian AFF_2:def 2 :
for AP being AffinSpace holds
( AP is Pappian iff for M, N being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9 );
definition
let AP be
AffinPlane;
attr AP is
satisfying_PAP_1 means :
Def3:
for
M,
N being
Subset of
AP for
o,
a,
b,
c,
a9,
b9,
c9 being
Element of
AP st
M is
being_line &
N is
being_line &
M <> N &
o in M &
o in N &
o <> a &
o <> a9 &
o <> b &
o <> b9 &
o <> c &
o <> c9 &
a in M &
b in M &
c in M &
b9 in N &
c9 in N &
a,
b9 // b,
a9 &
b,
c9 // c,
b9 &
a,
c9 // c,
a9 &
b <> c holds
a9 in N;
end;
::
deftheorem Def3 defines
satisfying_PAP_1 AFF_2:def 3 :
for AP being AffinPlane holds
( AP is satisfying_PAP_1 iff for M, N being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & b <> c holds
a9 in N );
definition
let AP be
AffinSpace;
attr AP is
Desarguesian means :
Def4:
for
A,
P,
C being
Subset of
AP for
o,
a,
b,
c,
a9,
b9,
c9 being
Element of
AP st
o in A &
o in P &
o in C &
o <> a &
o <> b &
o <> c &
a in A &
a9 in A &
b in P &
b9 in P &
c in C &
c9 in C &
A is
being_line &
P is
being_line &
C is
being_line &
A <> P &
A <> C &
a,
b // a9,
b9 &
a,
c // a9,
c9 holds
b,
c // b9,
c9;
end;
::
deftheorem Def4 defines
Desarguesian AFF_2:def 4 :
for AP being AffinSpace holds
( AP is Desarguesian iff for A, P, C being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 );
definition
let AP be
AffinPlane;
attr AP is
satisfying_DES_1 means :
Def5:
for
A,
P,
C being
Subset of
AP for
o,
a,
b,
c,
a9,
b9,
c9 being
Element of
AP st
o in A &
o in P &
o <> a &
o <> b &
o <> c &
a in A &
a9 in A &
b in P &
b9 in P &
c in C &
c9 in C &
A is
being_line &
P is
being_line &
C is
being_line &
A <> P &
A <> C &
a,
b // a9,
b9 &
a,
c // a9,
c9 &
b,
c // b9,
c9 & not
LIN a,
b,
c &
c <> c9 holds
o in C;
end;
::
deftheorem Def5 defines
satisfying_DES_1 AFF_2:def 5 :
for AP being AffinPlane holds
( AP is satisfying_DES_1 iff for A, P, C being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & not LIN a,b,c & c <> c9 holds
o in C );
definition
let AP be
AffinPlane;
attr AP is
satisfying_DES_2 means
for
A,
P,
C being
Subset of
AP for
o,
a,
b,
c,
a9,
b9,
c9 being
Element of
AP st
o in A &
o in P &
o in C &
o <> a &
o <> b &
o <> c &
a in A &
a9 in A &
b in P &
b9 in P &
c in C &
A is
being_line &
P is
being_line &
C is
being_line &
A <> P &
A <> C &
a,
b // a9,
b9 &
a,
c // a9,
c9 &
b,
c // b9,
c9 holds
c9 in C;
end;
::
deftheorem defines
satisfying_DES_2 AFF_2:def 6 :
for AP being AffinPlane holds
( AP is satisfying_DES_2 iff for A, P, C being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 holds
c9 in C );
definition
let AP be
AffinSpace;
attr AP is
Moufangian means :
Def7:
for
K being
Subset of
AP for
o,
a,
b,
c,
a9,
b9,
c9 being
Element of
AP st
K is
being_line &
o in K &
c in K &
c9 in K & not
a in K &
o <> c &
a <> b &
LIN o,
a,
a9 &
LIN o,
b,
b9 &
a,
b // a9,
b9 &
a,
c // a9,
c9 &
a,
b // K holds
b,
c // b9,
c9;
end;
::
deftheorem Def7 defines
Moufangian AFF_2:def 7 :
for AP being AffinSpace holds
( AP is Moufangian iff for K being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & a,b // K holds
b,c // b9,c9 );
definition
let AP be
AffinPlane;
attr AP is
satisfying_TDES_1 means :
Def8:
for
K being
Subset of
AP for
o,
a,
b,
c,
a9,
b9,
c9 being
Element of
AP st
K is
being_line &
o in K &
c in K &
c9 in K & not
a in K &
o <> c &
a <> b &
LIN o,
a,
a9 &
a,
b // a9,
b9 &
b,
c // b9,
c9 &
a,
c // a9,
c9 &
a,
b // K holds
LIN o,
b,
b9;
end;
::
deftheorem Def8 defines
satisfying_TDES_1 AFF_2:def 8 :
for AP being AffinPlane holds
( AP is satisfying_TDES_1 iff for K being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & a,b // a9,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K holds
LIN o,b,b9 );
definition
let AP be
AffinPlane;
attr AP is
satisfying_TDES_2 means :
Def9:
for
K being
Subset of
AP for
o,
a,
b,
c,
a9,
b9,
c9 being
Element of
AP st
K is
being_line &
o in K &
c in K &
c9 in K & not
a in K &
o <> c &
a <> b &
LIN o,
a,
a9 &
LIN o,
b,
b9 &
b,
c // b9,
c9 &
a,
c // a9,
c9 &
a,
b // K holds
a,
b // a9,
b9;
end;
::
deftheorem Def9 defines
satisfying_TDES_2 AFF_2:def 9 :
for AP being AffinPlane holds
( AP is satisfying_TDES_2 iff for K being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K holds
a,b // a9,b9 );
definition
let AP be
AffinPlane;
attr AP is
satisfying_TDES_3 means :
Def10:
for
K being
Subset of
AP for
o,
a,
b,
c,
a9,
b9,
c9 being
Element of
AP st
K is
being_line &
o in K &
c in K & not
a in K &
o <> c &
a <> b &
LIN o,
a,
a9 &
LIN o,
b,
b9 &
a,
b // a9,
b9 &
a,
c // a9,
c9 &
b,
c // b9,
c9 &
a,
b // K holds
c9 in K;
end;
::
deftheorem Def10 defines
satisfying_TDES_3 AFF_2:def 10 :
for AP being AffinPlane holds
( AP is satisfying_TDES_3 iff for K being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st K is being_line & o in K & c in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & a,b // K holds
c9 in K );
definition
let AP be
AffinSpace;
attr AP is
translational means :
Def11:
for
A,
P,
C being
Subset of
AP for
a,
b,
c,
a9,
b9,
c9 being
Element of
AP st
A // P &
A // C &
a in A &
a9 in A &
b in P &
b9 in P &
c in C &
c9 in C &
A is
being_line &
P is
being_line &
C is
being_line &
A <> P &
A <> C &
a,
b // a9,
b9 &
a,
c // a9,
c9 holds
b,
c // b9,
c9;
end;
::
deftheorem Def11 defines
translational AFF_2:def 11 :
for AP being AffinSpace holds
( AP is translational iff for A, P, C being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 );
definition
let AP be
AffinPlane;
attr AP is
satisfying_des_1 means :
Def12:
for
A,
P,
C being
Subset of
AP for
a,
b,
c,
a9,
b9,
c9 being
Element of
AP st
A // P &
a in A &
a9 in A &
b in P &
b9 in P &
c in C &
c9 in C &
A is
being_line &
P is
being_line &
C is
being_line &
A <> P &
A <> C &
a,
b // a9,
b9 &
a,
c // a9,
c9 &
b,
c // b9,
c9 & not
LIN a,
b,
c &
c <> c9 holds
A // C;
end;
::
deftheorem Def12 defines
satisfying_des_1 AFF_2:def 12 :
for AP being AffinPlane holds
( AP is satisfying_des_1 iff for A, P, C being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st A // P & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & not LIN a,b,c & c <> c9 holds
A // C );
definition
let AP be
AffinSpace;
attr AP is
satisfying_pap means :
Def13:
for
M,
N being
Subset of
AP for
a,
b,
c,
a9,
b9,
c9 being
Element of
AP st
M is
being_line &
N is
being_line &
a in M &
b in M &
c in M &
M // N &
M <> N &
a9 in N &
b9 in N &
c9 in N &
a,
b9 // b,
a9 &
b,
c9 // c,
b9 holds
a,
c9 // c,
a9;
end;
::
deftheorem Def13 defines
satisfying_pap AFF_2:def 13 :
for AP being AffinSpace holds
( AP is satisfying_pap iff for M, N being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9 );
definition
let AP be
AffinPlane;
attr AP is
satisfying_pap_1 means :
Def14:
for
M,
N being
Subset of
AP for
a,
b,
c,
a9,
b9,
c9 being
Element of
AP st
M is
being_line &
N is
being_line &
a in M &
b in M &
c in M &
M // N &
M <> N &
a9 in N &
b9 in N &
a,
b9 // b,
a9 &
b,
c9 // c,
b9 &
a,
c9 // c,
a9 &
a9 <> b9 holds
c9 in N;
end;
::
deftheorem Def14 defines
satisfying_pap_1 AFF_2:def 14 :
for AP being AffinPlane holds
( AP is satisfying_pap_1 iff for M, N being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & a9 <> b9 holds
c9 in N );