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 );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem Th17:
theorem
theorem
theorem
theorem Th21:
theorem
theorem Th23:
theorem Th24:
theorem
theorem
theorem Th27:
theorem
theorem