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

begin

definition

let AP be AffinPlane;
attr AP is satisfying_DES1 means :Def1: :: 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 Def1 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 :Def2: :: 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 Def2 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 :Def3: :: 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 Def3 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 :Def4: :: 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 Def4 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 :Def5: :: 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 Def5 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 :Def6: :: 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 Def6 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 :Def7: :: 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 Def7 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 :Def8: :: 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 Def8 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

canceled;

theorem :: AFF_3:2

canceled;

theorem :: AFF_3:3

canceled;

theorem :: AFF_3:4

canceled;

theorem :: AFF_3:5

canceled;

theorem :: AFF_3:6

canceled;

theorem :: AFF_3:7

canceled;

theorem :: AFF_3:8

canceled;

theorem :: AFF_3:9

for AP being AffinPlane st AP is satisfying_DES1 holds
AP is satisfying_DES1_1

proof end;

theorem :: AFF_3:10

for AP being AffinPlane st AP is satisfying_DES1_1 holds
AP is satisfying_DES1

proof end;

theorem :: AFF_3:11

for AP being AffinPlane st AP is Desarguesian holds
AP is satisfying_DES1

proof end;

theorem :: AFF_3:12

for AP being AffinPlane st AP is Desarguesian holds
AP is satisfying_DES1_2

proof end;

theorem :: AFF_3:13

for AP being AffinPlane st AP is satisfying_DES1_2 holds
AP is satisfying_DES1_3

proof end;

theorem :: AFF_3:14

for AP being AffinPlane st AP is satisfying_DES1_2 holds
AP is Desarguesian

proof end;

theorem :: AFF_3:15

for AP being AffinPlane st AP is satisfying_DES2_1 holds
AP is satisfying_DES2

proof end;

theorem :: AFF_3:16

for AP being AffinPlane holds
( AP is satisfying_DES2_1 iff AP is satisfying_DES2_3 )

proof end;

theorem :: AFF_3:17

for AP being AffinPlane holds
( AP is satisfying_DES2 iff AP is satisfying_DES2_2 )

proof end;

theorem :: AFF_3:18

for AP being AffinPlane st AP is satisfying_DES1_3 holds
AP is satisfying_DES2_1

proof end;