:: Metric-Affine Configurations in Metric Affine Planes - Part I
:: by Jolanta \'Swierzy\'nska and Bogdan \'Swierzy\'nski
::
:: Received October 31, 1990
:: Copyright (c) 1990-2011 Association of Mizar Users

begin

definition

let X be OrtAfPl;
attr X is satisfying_DES means :: CONAFFM:def 1
for o, a, a1, b, b1, c, c1 being Element of X st o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & not LIN b,b1,a & not LIN a,a1,c & LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1 & a,b // a1,b1 & a,c // a1,c1 holds
b,c // b1,c1;
attr X is satisfying_AH means :: CONAFFM:def 2
for o, a, a1, b, b1, c, c1 being Element of X st o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & o,a // b,c & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b holds
b,c _|_ b1,c1;
attr X is satisfying_3H means :: CONAFFM:def 3
for a, b, c being Element of X st not LIN a,b,c holds
ex d being Element of X st
( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b );
attr X is satisfying_ODES means :Def4: :: CONAFFM:def 4
for o, a, a1, b, b1, c, c1 being Element of X st o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b holds
b,c _|_ b1,c1;
attr X is satisfying_LIN means :Def5: :: CONAFFM:def 5
for o, a, a1, b, b1, c, c1 being Element of X st o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & a <> b & o,c _|_ o,c1 & o,a _|_ o,a1 & o,b _|_ o,b1 & not LIN o,c,a & LIN o,a,b & LIN o,a1,b1 & a,c _|_ a1,c1 & b,c _|_ b1,c1 holds
a,a1 // b,b1;
attr X is satisfying_LIN1 means :Def6: :: CONAFFM:def 6
for o, a, a1, b, b1, c, c1 being Element of X st o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & a <> b & o,c _|_ o,c1 & o,a _|_ o,a1 & o,b _|_ o,b1 & not LIN o,c,a & LIN o,a,b & LIN o,a1,b1 & a,c _|_ a1,c1 & a,a1 // b,b1 holds
b,c _|_ b1,c1;
attr X is satisfying_LIN2 means :: CONAFFM:def 7
for o, a, a1, b, b1, c, c1 being Element of X st o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & a <> b & a,a1 // b,b1 & o,a _|_ o,a1 & o,b _|_ o,b1 & not LIN o,c,a & LIN o,a,b & LIN o,a1,b1 & a,c _|_ a1,c1 & b,c _|_ b1,c1 holds
o,c _|_ o,c1;

end;

:: deftheorem defines satisfying_DES CONAFFM:def 1 :
for X being OrtAfPl holds
( X is satisfying_DES iff for o, a, a1, b, b1, c, c1 being Element of X st o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & not LIN b,b1,a & not LIN a,a1,c & LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1 & a,b // a1,b1 & a,c // a1,c1 holds
b,c // b1,c1 );

:: deftheorem defines satisfying_AH CONAFFM:def 2 :
for X being OrtAfPl holds
( X is satisfying_AH iff for o, a, a1, b, b1, c, c1 being Element of X st o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & o,a // b,c & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b holds
b,c _|_ b1,c1 );

:: deftheorem defines satisfying_3H CONAFFM:def 3 :
for X being OrtAfPl holds
( X is satisfying_3H iff for a, b, c being Element of X st not LIN a,b,c holds
ex d being Element of X st
( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b ) );

:: deftheorem Def4 defines satisfying_ODES CONAFFM:def 4 :
for X being OrtAfPl holds
( X is satisfying_ODES iff for o, a, a1, b, b1, c, c1 being Element of X st o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b holds
b,c _|_ b1,c1 );

:: deftheorem Def5 defines satisfying_LIN CONAFFM:def 5 :
for X being OrtAfPl holds
( X is satisfying_LIN iff for o, a, a1, b, b1, c, c1 being Element of X st o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & a <> b & o,c _|_ o,c1 & o,a _|_ o,a1 & o,b _|_ o,b1 & not LIN o,c,a & LIN o,a,b & LIN o,a1,b1 & a,c _|_ a1,c1 & b,c _|_ b1,c1 holds
a,a1 // b,b1 );

:: deftheorem Def6 defines satisfying_LIN1 CONAFFM:def 6 :
for X being OrtAfPl holds
( X is satisfying_LIN1 iff for o, a, a1, b, b1, c, c1 being Element of X st o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & a <> b & o,c _|_ o,c1 & o,a _|_ o,a1 & o,b _|_ o,b1 & not LIN o,c,a & LIN o,a,b & LIN o,a1,b1 & a,c _|_ a1,c1 & a,a1 // b,b1 holds
b,c _|_ b1,c1 );

:: deftheorem defines satisfying_LIN2 CONAFFM:def 7 :
for X being OrtAfPl holds
( X is satisfying_LIN2 iff for o, a, a1, b, b1, c, c1 being Element of X st o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & a <> b & a,a1 // b,b1 & o,a _|_ o,a1 & o,b _|_ o,b1 & not LIN o,c,a & LIN o,a,b & LIN o,a1,b1 & a,c _|_ a1,c1 & b,c _|_ b1,c1 holds
o,c _|_ o,c1 );

theorem :: CONAFFM:1

for X being OrtAfPl st X is satisfying_ODES holds
X is satisfying_DES

proof end;

theorem :: CONAFFM:2

for X being OrtAfPl st X is satisfying_ODES holds
X is satisfying_AH

proof end;

theorem Th3: :: CONAFFM:3

for X being OrtAfPl st X is satisfying_LIN holds
X is satisfying_LIN1

proof end;

theorem :: CONAFFM:4

for X being OrtAfPl st X is satisfying_LIN1 holds
X is satisfying_LIN2

proof end;

theorem :: CONAFFM:5

for X being OrtAfPl st X is satisfying_LIN holds
X is satisfying_ODES

proof end;

theorem :: CONAFFM:6

for X being OrtAfPl st X is satisfying_LIN holds
X is satisfying_3H

proof end;