:: AFF_2 semantic presentation

definition

let c₁ be AffinPlane;
attr a₁ is satisfying_PPAP means :Def1: :: AFF_2:def 1
for b₁, b₂ being Subset of a₁
for b₃, b₄, b₅, b₆, b₇, b₈ being Element of a₁ st b₁ is_line & b₂ is_line & b₃ in b₁ & b₄ in b₁ & b₅ in b₁ & b₆ in b₂ & b₇ in b₂ & b₈ in b₂ & b₃,b₇ // b₄,b₆ & b₄,b₈ // b₅,b₇ holds
b₃,b₈ // b₅,b₆;

end;

:: deftheorem Def1 defines satisfying_PPAP AFF_2:def 1 :

notation

let c₁ be AffinPlane;
synonym c₁ satisfies_PPAP for satisfying_PPAP c₁;

end;

definition

let c₁ be AffinSpace;
attr a₁ is Pappian means :Def2: :: AFF_2:def 2
for b₁, b₂ being Subset of a₁
for b₃, b₄, b₅, b₆, b₇, b₈, b₉ being Element of a₁ st b₁ is_line & b₂ is_line & b₁ <> b₂ & b₃ in b₁ & b₃ in b₂ & b₃ <> b₄ & b₃ <> b₇ & b₃ <> b₅ & b₃ <> b₈ & b₃ <> b₆ & b₃ <> b₉ & b₄ in b₁ & b₅ in b₁ & b₆ in b₁ & b₇ in b₂ & b₈ in b₂ & b₉ in b₂ & b₄,b₈ // b₅,b₇ & b₅,b₉ // b₆,b₈ holds
b₄,b₉ // b₆,b₇;

end;

:: deftheorem Def2 defines Pappian AFF_2:def 2 :

notation

let c₁ be AffinSpace;
synonym c₁ satisfies_PAP for Pappian c₁;

end;

definition

let c₁ be AffinPlane;
attr a₁ is satisfying_PAP_1 means :Def3: :: AFF_2:def 3
for b₁, b₂ being Subset of a₁
for b₃, b₄, b₅, b₆, b₇, b₈, b₉ being Element of a₁ st b₁ is_line & b₂ is_line & b₁ <> b₂ & b₃ in b₁ & b₃ in b₂ & b₃ <> b₄ & b₃ <> b₇ & b₃ <> b₅ & b₃ <> b₈ & b₃ <> b₆ & b₃ <> b₉ & b₄ in b₁ & b₅ in b₁ & b₆ in b₁ & b₈ in b₂ & b₉ in b₂ & b₄,b₈ // b₅,b₇ & b₅,b₉ // b₆,b₈ & b₄,b₉ // b₆,b₇ & b₅ <> b₆ holds
b₇ in b₂;

end;

:: deftheorem Def3 defines satisfying_PAP_1 AFF_2:def 3 :

notation

let c₁ be AffinPlane;
synonym c₁ satisfies_PAP_1 for satisfying_PAP_1 c₁;

end;

definition

let c₁ be AffinSpace;
attr a₁ is Desarguesian means :Def4: :: AFF_2:def 4
for b₁, b₂, b₃ being Subset of a₁
for b₄, b₅, b₆, b₇, b₈, b₉, b₁₀ being Element of a₁ st b₄ in b₁ & b₄ in b₂ & b₄ in b₃ & b₄ <> b₅ & b₄ <> b₆ & b₄ <> b₇ & b₅ in b₁ & b₈ in b₁ & b₆ in b₂ & b₉ in b₂ & b₇ in b₃ & b₁₀ in b₃ & b₁ is_line & b₂ is_line & b₃ is_line & b₁ <> b₂ & b₁ <> b₃ & b₅,b₆ // b₈,b₉ & b₅,b₇ // b₈,b₁₀ holds
b₆,b₇ // b₉,b₁₀;

end;

:: deftheorem Def4 defines Desarguesian AFF_2:def 4 :

notation

let c₁ be AffinSpace;
synonym c₁ satisfies_DES for Desarguesian c₁;

end;

definition

let c₁ be AffinPlane;
attr a₁ is satisfying_DES_1 means :Def5: :: AFF_2:def 5
for b₁, b₂, b₃ being Subset of a₁
for b₄, b₅, b₆, b₇, b₈, b₉, b₁₀ being Element of a₁ st b₄ in b₁ & b₄ in b₂ & b₄ <> b₅ & b₄ <> b₆ & b₄ <> b₇ & b₅ in b₁ & b₈ in b₁ & b₆ in b₂ & b₉ in b₂ & b₇ in b₃ & b₁₀ in b₃ & b₁ is_line & b₂ is_line & b₃ is_line & b₁ <> b₂ & b₁ <> b₃ & b₅,b₆ // b₈,b₉ & b₅,b₇ // b₈,b₁₀ & b₆,b₇ // b₉,b₁₀ & not LIN b₅,b₆,b₇ & b₇ <> b₁₀ holds
b₄ in b₃;

end;

:: deftheorem Def5 defines satisfying_DES_1 AFF_2:def 5 :

notation

let c₁ be AffinPlane;
synonym c₁ satisfies_DES_1 for satisfying_DES_1 c₁;

end;

definition

let c₁ be AffinPlane;
attr a₁ is satisfying_DES_2 means :: AFF_2:def 6
for b₁, b₂, b₃ being Subset of a₁
for b₄, b₅, b₆, b₇, b₈, b₉, b₁₀ being Element of a₁ st b₄ in b₁ & b₄ in b₂ & b₄ in b₃ & b₄ <> b₅ & b₄ <> b₆ & b₄ <> b₇ & b₅ in b₁ & b₈ in b₁ & b₆ in b₂ & b₉ in b₂ & b₇ in b₃ & b₁ is_line & b₂ is_line & b₃ is_line & b₁ <> b₂ & b₁ <> b₃ & b₅,b₆ // b₈,b₉ & b₅,b₇ // b₈,b₁₀ & b₆,b₇ // b₉,b₁₀ holds
b₁₀ in b₃;

end;

:: deftheorem Def6 defines satisfying_DES_2 AFF_2:def 6 :

notation

let c₁ be AffinPlane;
synonym c₁ satisfies_DES_2 for satisfying_DES_2 c₁;

end;

definition

let c₁ be AffinSpace;
attr a₁ is Moufangian means :Def7: :: AFF_2:def 7
for b₁ being Subset of a₁
for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of a₁ st b₁ is_line & b₂ in b₁ & b₅ in b₁ & b₈ in b₁ & not b₃ in b₁ & b₂ <> b₅ & b₃ <> b₄ & LIN b₂,b₃,b₆ & LIN b₂,b₄,b₇ & b₃,b₄ // b₆,b₇ & b₃,b₅ // b₆,b₈ & b₃,b₄ // b₁ holds
b₄,b₅ // b₇,b₈;

end;

:: deftheorem Def7 defines Moufangian AFF_2:def 7 :

notation

let c₁ be AffinSpace;
synonym c₁ satisfies_TDES for Moufangian c₁;

end;

definition

let c₁ be AffinPlane;
attr a₁ is satisfying_TDES_1 means :Def8: :: AFF_2:def 8
for b₁ being Subset of a₁
for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of a₁ st b₁ is_line & b₂ in b₁ & b₅ in b₁ & b₈ in b₁ & not b₃ in b₁ & b₂ <> b₅ & b₃ <> b₄ & LIN b₂,b₃,b₆ & b₃,b₄ // b₆,b₇ & b₄,b₅ // b₇,b₈ & b₃,b₅ // b₆,b₈ & b₃,b₄ // b₁ holds
LIN b₂,b₄,b₇;

end;

:: deftheorem Def8 defines satisfying_TDES_1 AFF_2:def 8 :

notation

let c₁ be AffinPlane;
synonym c₁ satisfies_TDES_1 for satisfying_TDES_1 c₁;

end;

definition

let c₁ be AffinPlane;
attr a₁ is satisfying_TDES_2 means :Def9: :: AFF_2:def 9
for b₁ being Subset of a₁
for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of a₁ st b₁ is_line & b₂ in b₁ & b₅ in b₁ & b₈ in b₁ & not b₃ in b₁ & b₂ <> b₅ & b₃ <> b₄ & LIN b₂,b₃,b₆ & LIN b₂,b₄,b₇ & b₄,b₅ // b₇,b₈ & b₃,b₅ // b₆,b₈ & b₃,b₄ // b₁ holds
b₃,b₄ // b₆,b₇;

end;

:: deftheorem Def9 defines satisfying_TDES_2 AFF_2:def 9 :

notation

let c₁ be AffinPlane;
synonym c₁ satisfies_TDES_2 for satisfying_TDES_2 c₁;

end;

definition

let c₁ be AffinPlane;
attr a₁ is satisfying_TDES_3 means :Def10: :: AFF_2:def 10
for b₁ being Subset of a₁
for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of a₁ st b₁ is_line & b₂ in b₁ & b₅ in b₁ & not b₃ in b₁ & b₂ <> b₅ & b₃ <> b₄ & LIN b₂,b₃,b₆ & LIN b₂,b₄,b₇ & b₃,b₄ // b₆,b₇ & b₃,b₅ // b₆,b₈ & b₄,b₅ // b₇,b₈ & b₃,b₄ // b₁ holds
b₈ in b₁;

end;

:: deftheorem Def10 defines satisfying_TDES_3 AFF_2:def 10 :

notation

let c₁ be AffinPlane;
synonym c₁ satisfies_TDES_3 for satisfying_TDES_3 c₁;

end;

definition

let c₁ be AffinSpace;
attr a₁ is translational means :Def11: :: AFF_2:def 11
for b₁, b₂, b₃ being Subset of a₁
for b₄, b₅, b₆, b₇, b₈, b₉ being Element of a₁ st b₁ // b₂ & b₁ // b₃ & b₄ in b₁ & b₇ in b₁ & b₅ in b₂ & b₈ in b₂ & b₆ in b₃ & b₉ in b₃ & b₁ is_line & b₂ is_line & b₃ is_line & b₁ <> b₂ & b₁ <> b₃ & b₄,b₅ // b₇,b₈ & b₄,b₆ // b₇,b₉ holds
b₅,b₆ // b₈,b₉;

end;

:: deftheorem Def11 defines translational AFF_2:def 11 :

notation

let c₁ be AffinSpace;
synonym c₁ satisfies_des for translational c₁;

end;

definition

let c₁ be AffinPlane;
attr a₁ is satisfying_des_1 means :Def12: :: AFF_2:def 12
for b₁, b₂, b₃ being Subset of a₁
for b₄, b₅, b₆, b₇, b₈, b₉ being Element of a₁ st b₁ // b₂ & b₄ in b₁ & b₇ in b₁ & b₅ in b₂ & b₈ in b₂ & b₆ in b₃ & b₉ in b₃ & b₁ is_line & b₂ is_line & b₃ is_line & b₁ <> b₂ & b₁ <> b₃ & b₄,b₅ // b₇,b₈ & b₄,b₆ // b₇,b₉ & b₅,b₆ // b₈,b₉ & not LIN b₄,b₅,b₆ & b₆ <> b₉ holds
b₁ // b₃;

end;

:: deftheorem Def12 defines satisfying_des_1 AFF_2:def 12 :

notation

let c₁ be AffinPlane;
synonym c₁ satisfies_des_1 for satisfying_des_1 c₁;

end;

definition

let c₁ be AffinSpace;
attr a₁ is satisfying_pap means :Def13: :: AFF_2:def 13
for b₁, b₂ being Subset of a₁
for b₃, b₄, b₅, b₆, b₇, b₈ being Element of a₁ st b₁ is_line & b₂ is_line & b₃ in b₁ & b₄ in b₁ & b₅ in b₁ & b₁ // b₂ & b₁ <> b₂ & b₆ in b₂ & b₇ in b₂ & b₈ in b₂ & b₃,b₇ // b₄,b₆ & b₄,b₈ // b₅,b₇ holds
b₃,b₈ // b₅,b₆;

end;

:: deftheorem Def13 defines satisfying_pap AFF_2:def 13 :

notation

let c₁ be AffinSpace;
synonym c₁ satisfies_pap for satisfying_pap c₁;

end;

definition

let c₁ be AffinPlane;
attr a₁ is satisfying_pap_1 means :Def14: :: AFF_2:def 14
for b₁, b₂ being Subset of a₁
for b₃, b₄, b₅, b₆, b₇, b₈ being Element of a₁ st b₁ is_line & b₂ is_line & b₃ in b₁ & b₄ in b₁ & b₅ in b₁ & b₁ // b₂ & b₁ <> b₂ & b₆ in b₂ & b₇ in b₂ & b₃,b₇ // b₄,b₆ & b₄,b₈ // b₅,b₇ & b₃,b₈ // b₅,b₆ & b₆ <> b₇ holds
b₈ in b₂;

end;

:: deftheorem Def14 defines satisfying_pap_1 AFF_2:def 14 :

notation

let c₁ be AffinPlane;
synonym c₁ satisfies_pap_1 for satisfying_pap_1 c₁;

end;

theorem Th1: :: AFF_2:1

canceled;

theorem Th2: :: AFF_2:2

canceled;

theorem Th3: :: AFF_2:3

canceled;

theorem Th4: :: AFF_2:4

canceled;

theorem Th5: :: AFF_2:5

canceled;

theorem Th6: :: AFF_2:6

canceled;

theorem Th7: :: AFF_2:7

canceled;

theorem Th8: :: AFF_2:8

canceled;

theorem Th9: :: AFF_2:9

canceled;

theorem Th10: :: AFF_2:10

canceled;

theorem Th11: :: AFF_2:11

canceled;

theorem Th12: :: AFF_2:12

canceled;

theorem Th13: :: AFF_2:13

canceled;

theorem Th14: :: AFF_2:14

canceled;

theorem Th15: :: AFF_2:15

for b₁ being AffinPlane holds
( b₁ satisfies_PAP iff b₁ satisfies_PAP_1 )

proof end;

theorem Th16: :: AFF_2:16

for b₁ being AffinPlane holds
( b₁ satisfies_DES iff b₁ satisfies_DES_1 )

proof end;

theorem Th17: :: AFF_2:17

for b₁ being AffinPlane st b₁ satisfies_TDES holds
b₁ satisfies_TDES_1

proof end;

theorem Th18: :: AFF_2:18

for b₁ being AffinPlane st b₁ satisfies_TDES_1 holds
b₁ satisfies_TDES_2

proof end;

theorem Th19: :: AFF_2:19

for b₁ being AffinPlane st b₁ satisfies_TDES_2 holds
b₁ satisfies_TDES_3

proof end;

theorem Th20: :: AFF_2:20

for b₁ being AffinPlane st b₁ satisfies_TDES_3 holds
b₁ satisfies_TDES

proof end;

theorem Th21: :: AFF_2:21

for b₁ being AffinPlane holds
( b₁ satisfies_des iff b₁ satisfies_des_1 )

proof end;

theorem Th22: :: AFF_2:22

for b₁ being AffinPlane holds
( b₁ satisfies_pap iff b₁ satisfies_pap_1 )

proof end;

theorem Th23: :: AFF_2:23

for b₁ being AffinPlane st b₁ satisfies_PAP holds
b₁ satisfies_pap

proof end;

theorem Th24: :: AFF_2:24

for b₁ being AffinPlane holds
( b₁ satisfies_PPAP iff ( b₁ satisfies_PAP & b₁ satisfies_pap ) )

proof end;

theorem Th25: :: AFF_2:25

for b₁ being AffinPlane st b₁ satisfies_PAP holds
b₁ satisfies_DES

proof end;

theorem Th26: :: AFF_2:26

for b₁ being AffinPlane st b₁ satisfies_DES holds
b₁ satisfies_TDES

proof end;

theorem Th27: :: AFF_2:27

for b₁ being AffinPlane st b₁ satisfies_TDES_1 holds
b₁ satisfies_des_1

proof end;

theorem Th28: :: AFF_2:28

for b₁ being AffinPlane st b₁ satisfies_TDES holds
b₁ satisfies_des

proof end;

theorem Th29: :: AFF_2:29

for b₁ being AffinPlane st b₁ satisfies_des holds
b₁ satisfies_pap

proof end;