:: Affine Localizations of Desargues Axiom
:: by Eugeniusz Kusak, Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Copyright (c) 1990-2021 Association of Mizar Users

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

:: deftheorem 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, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds
a,c // p,q );

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

:: deftheorem 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, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & c <> q & not LIN b,a,c & not LIN b9,a9,c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds
a,c // a9,c9 );

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

:: deftheorem 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, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds
o in C );

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

:: deftheorem 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, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & b <> b9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds
o in P );

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

:: deftheorem 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, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds
a,c // p,q );

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

:: deftheorem 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, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds
a,c // a9,c9 );

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

:: deftheorem 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, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds
A // P );

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

:: deftheorem 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, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds
A // C );

theorem :: AFF_3:1
for AP being AffinPlane st AP is satisfying_DES1 holds
AP is satisfying_DES1_1
proof end;

theorem :: AFF_3:2
for AP being AffinPlane st AP is satisfying_DES1_1 holds
AP is satisfying_DES1
proof end;

theorem :: AFF_3:3
for AP being AffinPlane st AP is Desarguesian holds
AP is satisfying_DES1
proof end;

theorem :: AFF_3:4
for AP being AffinPlane st AP is Desarguesian holds
AP is satisfying_DES1_2
proof end;

theorem :: AFF_3:5
for AP being AffinPlane st AP is satisfying_DES1_2 holds
AP is satisfying_DES1_3
proof end;

theorem :: AFF_3:6
for AP being AffinPlane st AP is satisfying_DES1_2 holds
AP is Desarguesian
proof end;

theorem :: AFF_3:7
for AP being AffinPlane st AP is satisfying_DES2_1 holds
AP is satisfying_DES2
proof end;

theorem :: AFF_3:8
for AP being AffinPlane holds
( AP is satisfying_DES2_1 iff AP is satisfying_DES2_3 )
proof end;

theorem :: AFF_3:9
for AP being AffinPlane holds
( AP is satisfying_DES2 iff AP is satisfying_DES2_2 )
proof end;

theorem :: AFF_3:10
for AP being AffinPlane st AP is satisfying_DES1_3 holds
AP is satisfying_DES2_1
proof end;