:: Classical Configurations in Affine Planes
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Copyright (c) 1990-2021 Association of Mizar Users

definition
let AP be AffinPlane;
attr AP is satisfying_PPAP means :: AFF_2:def 1
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 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 :: AFF_2:def 2
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 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 :: AFF_2:def 3
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 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 :: AFF_2:def 4
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 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 :: AFF_2:def 5
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 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 :: AFF_2:def 6
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 :: AFF_2:def 7
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 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 :: AFF_2:def 8
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 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 :: AFF_2:def 9
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 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 :: AFF_2:def 10
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 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 :: AFF_2:def 11
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 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 :: AFF_2:def 12
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 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 :: AFF_2:def 13
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 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 :: AFF_2:def 14
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 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 :: AFF_2:1
for AP being AffinPlane holds
( AP is Pappian iff AP is satisfying_PAP_1 )
proof end;

theorem :: AFF_2:2
for AP being AffinPlane holds
( AP is Desarguesian iff AP is satisfying_DES_1 )
proof end;

theorem Th3: :: AFF_2:3
for AP being AffinPlane st AP is Moufangian holds
AP is satisfying_TDES_1
proof end;

theorem :: AFF_2:4
for AP being AffinPlane st AP is satisfying_TDES_1 holds
AP is satisfying_TDES_2
proof end;

theorem :: AFF_2:5
for AP being AffinPlane st AP is satisfying_TDES_2 holds
AP is satisfying_TDES_3
proof end;

theorem :: AFF_2:6
for AP being AffinPlane st AP is satisfying_TDES_3 holds
AP is Moufangian
proof end;

theorem Th7: :: AFF_2:7
for AP being AffinPlane holds
( AP is translational iff AP is satisfying_des_1 )
proof end;

theorem :: AFF_2:8
for AP being AffinPlane holds
( AP is satisfying_pap iff AP is satisfying_pap_1 )
proof end;

theorem Th9: :: AFF_2:9
for AP being AffinPlane st AP is Pappian holds
AP is satisfying_pap
proof end;

theorem Th10: :: AFF_2:10
for AP being AffinPlane holds
( AP is satisfying_PPAP iff ( AP is Pappian & AP is satisfying_pap ) )
proof end;

theorem :: AFF_2:11
for AP being AffinPlane st AP is Pappian holds
AP is Desarguesian
proof end;

theorem :: AFF_2:12
for AP being AffinPlane st AP is Desarguesian holds
AP is Moufangian
proof end;

theorem Th13: :: AFF_2:13
for AP being AffinPlane st AP is satisfying_TDES_1 holds
AP is satisfying_des_1
proof end;

theorem :: AFF_2:14
for AP being AffinPlane st AP is Moufangian holds
AP is translational
proof end;

theorem :: AFF_2:15
for AP being AffinPlane st AP is translational holds
AP is satisfying_pap
proof end;