:: Classical and Non--classical Pasch Configurations in Ordered Affine PlanesMa{\l}gorzata Pra\.zmowska
:: by Henryk Oryszczyszyn, Krzysztof Pra\.zmowski and
::
:: Received May 16, 1990
:: Copyright (c) 1990 Association of Mizar Users
definition
let OAS be
OAffinSpace;
attr OAS is
satisfying_Int_Par_Pasch means :: PASCH:def 1
for
a,
b,
c,
d,
p being
Element of
OAS st not
LIN p,
b,
c &
Mid b,
p,
a &
LIN p,
c,
d &
b,
c '||' d,
a holds
Mid c,
p,
d;
end;
:: deftheorem defines satisfying_Int_Par_Pasch PASCH:def 1 :
for
OAS being
OAffinSpace holds
(
OAS is
satisfying_Int_Par_Pasch iff for
a,
b,
c,
d,
p being
Element of
OAS st not
LIN p,
b,
c &
Mid b,
p,
a &
LIN p,
c,
d &
b,
c '||' d,
a holds
Mid c,
p,
d );
definition
let OAS be
OAffinSpace;
attr OAS is
satisfying_Ext_Par_Pasch means :: PASCH:def 2
for
a,
b,
c,
d,
p being
Element of
OAS st
Mid p,
b,
c &
LIN p,
a,
d &
a,
b '||' c,
d & not
LIN p,
a,
b holds
Mid p,
a,
d;
end;
:: deftheorem defines satisfying_Ext_Par_Pasch PASCH:def 2 :
for
OAS being
OAffinSpace holds
(
OAS is
satisfying_Ext_Par_Pasch iff for
a,
b,
c,
d,
p being
Element of
OAS st
Mid p,
b,
c &
LIN p,
a,
d &
a,
b '||' c,
d & not
LIN p,
a,
b holds
Mid p,
a,
d );
definition
let OAS be
OAffinSpace;
attr OAS is
satisfying_Gen_Par_Pasch means :: PASCH:def 3
for
a,
b,
c,
a',
b',
c' being
Element of
OAS st not
LIN a,
b,
a' &
a,
a' '||' b,
b' &
a,
a' '||' c,
c' &
Mid a,
b,
c &
LIN a',
b',
c' holds
Mid a',
b',
c';
end;
:: deftheorem defines satisfying_Gen_Par_Pasch PASCH:def 3 :
for
OAS being
OAffinSpace holds
(
OAS is
satisfying_Gen_Par_Pasch iff for
a,
b,
c,
a',
b',
c' being
Element of
OAS st not
LIN a,
b,
a' &
a,
a' '||' b,
b' &
a,
a' '||' c,
c' &
Mid a,
b,
c &
LIN a',
b',
c' holds
Mid a',
b',
c' );
definition
let OAS be
OAffinSpace;
attr OAS is
satisfying_Ext_Bet_Pasch means :: PASCH:def 4
for
a,
b,
c,
d,
x,
y being
Element of
OAS st
Mid a,
b,
d &
Mid b,
x,
c & not
LIN a,
b,
c holds
ex
y being
Element of
OAS st
(
Mid a,
y,
c &
Mid y,
x,
d );
end;
:: deftheorem defines satisfying_Ext_Bet_Pasch PASCH:def 4 :
for
OAS being
OAffinSpace holds
(
OAS is
satisfying_Ext_Bet_Pasch iff for
a,
b,
c,
d,
x,
y being
Element of
OAS st
Mid a,
b,
d &
Mid b,
x,
c & not
LIN a,
b,
c holds
ex
y being
Element of
OAS st
(
Mid a,
y,
c &
Mid y,
x,
d ) );
definition
let OAS be
OAffinSpace;
attr OAS is
satisfying_Int_Bet_Pasch means :: PASCH:def 5
for
a,
b,
c,
d,
x,
y being
Element of
OAS st
Mid a,
b,
d &
Mid a,
x,
c & not
LIN a,
b,
c holds
ex
y being
Element of
OAS st
(
Mid b,
y,
c &
Mid x,
y,
d );
end;
:: deftheorem defines satisfying_Int_Bet_Pasch PASCH:def 5 :
for
OAS being
OAffinSpace holds
(
OAS is
satisfying_Int_Bet_Pasch iff for
a,
b,
c,
d,
x,
y being
Element of
OAS st
Mid a,
b,
d &
Mid a,
x,
c & not
LIN a,
b,
c holds
ex
y being
Element of
OAS st
(
Mid b,
y,
c &
Mid x,
y,
d ) );
definition
let OAS be
OAffinSpace;
attr OAS is
Fanoian means :: PASCH:def 6
for
a,
b,
c,
d being
Element of
OAS st
a,
b // c,
d &
a,
c // b,
d & not
LIN a,
b,
c holds
ex
x being
Element of
OAS st
(
Mid a,
x,
d &
Mid b,
x,
c );
end;
:: deftheorem defines Fanoian PASCH:def 6 :
for
OAS being
OAffinSpace holds
(
OAS is
Fanoian iff for
a,
b,
c,
d being
Element of
OAS st
a,
b // c,
d &
a,
c // b,
d & not
LIN a,
b,
c holds
ex
x being
Element of
OAS st
(
Mid a,
x,
d &
Mid b,
x,
c ) );
theorem :: PASCH:1
canceled;
theorem :: PASCH:2
canceled;
theorem :: PASCH:3
canceled;
theorem :: PASCH:4
canceled;
theorem :: PASCH:5
canceled;
theorem :: PASCH:6
canceled;
theorem Th7: :: PASCH:7
theorem Th8: :: PASCH:8
theorem :: PASCH:9
theorem :: PASCH:10
canceled;
theorem Th11: :: PASCH:11
for
OAS being
OAffinSpace for
p,
a,
b,
c,
d1,
d2 being
Element of
OAS st not
LIN p,
a,
b &
LIN p,
b,
c &
LIN p,
a,
d1 &
LIN p,
a,
d2 &
a,
b '||' c,
d1 &
a,
b '||' c,
d2 holds
d1 = d2
theorem Th12: :: PASCH:12
for
OAS being
OAffinSpace for
a,
b,
c,
d1,
d2 being
Element of
OAS st not
LIN a,
b,
c &
a,
b '||' c,
d1 &
a,
b '||' c,
d2 &
a,
c '||' b,
d1 &
a,
c '||' b,
d2 holds
d1 = d2
theorem Th13: :: PASCH:13
for
OAS being
OAffinSpace for
p,
b,
c,
a,
d being
Element of
OAS st not
LIN p,
b,
c &
Mid b,
p,
a &
LIN p,
c,
d &
b,
c '||' d,
a holds
Mid c,
p,
d
theorem :: PASCH:14
theorem Th15: :: PASCH:15
for
OAS being
OAffinSpace for
p,
b,
c,
a,
d being
Element of
OAS st
Mid p,
b,
c &
LIN p,
a,
d &
a,
b '||' c,
d & not
LIN p,
a,
b holds
Mid p,
a,
d
theorem :: PASCH:16
theorem Th17: :: PASCH:17
for
OAS being
OAffinSpace for
a,
b,
a',
b',
c,
c' being
Element of
OAS st not
LIN a,
b,
a' &
a,
a' '||' b,
b' &
a,
a' '||' c,
c' &
Mid a,
b,
c &
LIN a',
b',
c' holds
Mid a',
b',
c'
theorem :: PASCH:18
theorem :: PASCH:19
for
OAS being
OAffinSpace for
p,
a,
b,
a',
b' being
Element of
OAS st not
LIN p,
a,
b &
a,
p // p,
a' &
b,
p // p,
b' &
a,
b '||' a',
b' holds
a,
b // b',
a'
theorem :: PASCH:20
for
OAS being
OAffinSpace for
p,
a,
a',
b,
b' being
Element of
OAS st not
LIN p,
a,
a' &
p,
a // p,
b &
p,
a' // p,
b' &
a,
a' '||' b,
b' holds
a,
a' // b,
b'
theorem Th21: :: PASCH:21
for
OAS being
OAffinSpace for
p,
a,
b,
c being
Element of
OAS st not
LIN p,
a,
b &
p,
a '||' b,
c &
p,
b '||' a,
c holds
(
p,
a // b,
c &
p,
b // a,
c )
theorem Th22: :: PASCH:22
for
OAS being
OAffinSpace for
p,
c,
b,
d,
a being
Element of
OAS st
Mid p,
c,
b &
c,
d // b,
a &
p,
d // p,
a & not
LIN p,
a,
b &
p <> c holds
Mid p,
d,
a
theorem Th23: :: PASCH:23
for
OAS being
OAffinSpace for
p,
d,
a,
c,
b being
Element of
OAS st
Mid p,
d,
a &
c,
d // b,
a &
p,
c // p,
b & not
LIN p,
a,
b &
p <> c holds
Mid p,
c,
b
theorem Th24: :: PASCH:24
for
OAS being
OAffinSpace for
p,
a,
b,
c,
d being
Element of
OAS st not
LIN p,
a,
b &
p,
b // p,
c &
b,
a // c,
d &
LIN a,
p,
d &
p <> d holds
not
Mid a,
p,
d
theorem Th25: :: PASCH:25
theorem Th26: :: PASCH:26
theorem Th27: :: PASCH:27
theorem Th28: :: PASCH:28
for
OAS being
OAffinSpace for
p,
a,
b,
c being
Element of
OAS st not
LIN p,
a,
b &
Mid p,
c,
b holds
ex
x being
Element of
OAS st
(
Mid p,
x,
a &
a,
b // x,
c )
theorem :: PASCH:29
theorem Th30: :: PASCH:30
for
OAS being
OAffinSpace for
a,
b,
c,
d being
Element of
OAS st
a,
b // c,
d & not
LIN a,
b,
c holds
ex
x being
Element of
OAS st
(
Mid a,
x,
d &
Mid b,
x,
c )
theorem :: PASCH:31
canceled;
theorem :: PASCH:32
theorem :: PASCH:33
for
OAS being
OAffinSpace for
a,
b,
c,
d being
Element of
OAS st
a,
b '||' c,
d &
a,
c '||' b,
d & not
LIN a,
b,
c holds
ex
x being
Element of
OAS st
(
LIN x,
a,
d &
LIN x,
b,
c )
theorem :: PASCH:34
for
OAS being
OAffinSpace for
a,
b,
c,
d,
p being
Element of
OAS st
a,
b '||' c,
d &
a,
c '||' b,
d & not
LIN a,
b,
c &
LIN p,
a,
d &
LIN p,
b,
c holds
not
LIN p,
a,
b
theorem Th35: :: PASCH:35
for
OAS being
OAffinSpace for
a,
b,
d,
x,
c being
Element of
OAS st
Mid a,
b,
d &
Mid b,
x,
c & not
LIN a,
b,
c holds
ex
y being
Element of
OAS st
(
Mid a,
y,
c &
Mid y,
x,
d )
theorem :: PASCH:36
theorem Th37: :: PASCH:37
for
OAS being
OAffinSpace for
a,
b,
d,
x,
c being
Element of
OAS st
Mid a,
b,
d &
Mid a,
x,
c & not
LIN a,
b,
c holds
ex
y being
Element of
OAS st
(
Mid b,
y,
c &
Mid x,
y,
d )
theorem :: PASCH:38
theorem :: PASCH:39
for
OAS being
OAffinSpace for
p,
a,
b,
p',
a',
b' being
Element of
OAS st
Mid p,
a,
b &
p,
a // p',
a' & not
LIN p,
a,
p' &
LIN p',
a',
b' &
p,
p' // a,
a' &
p,
p' // b,
b' holds
Mid p',
a',
b'