begin
definition
let X be
OrtAfPl;
attr X is
satisfying_OPAP means :
Def1:
for
o,
a1,
a2,
a3,
b1,
b2,
b3 being
Element of
for
M,
N being
Subset of st
o in M &
a1 in M &
a2 in M &
a3 in M &
o in N &
b1 in N &
b2 in N &
b3 in N & not
b2 in M & not
a3 in N &
M _|_ N &
o <> a1 &
o <> a2 &
o <> a3 &
o <> b1 &
o <> b2 &
o <> b3 &
a3,
b2 // a2,
b1 &
a3,
b3 // a1,
b1 holds
a1,
b2 // a2,
b3;
attr X is
satisfying_PAP means
for
o,
a1,
a2,
a3,
b1,
b2,
b3 being
Element of
for
M,
N being
Subset of st
M is
being_line &
N is
being_line &
o in M &
a1 in M &
a2 in M &
a3 in M &
o in N &
b1 in N &
b2 in N &
b3 in N & not
b2 in M & not
a3 in N &
o <> a1 &
o <> a2 &
o <> a3 &
o <> b1 &
o <> b2 &
o <> b3 &
a3,
b2 // a2,
b1 &
a3,
b3 // a1,
b1 holds
a1,
b2 // a2,
b3;
attr X is
satisfying_MH1 means :
Def3:
for
a1,
a2,
a3,
a4,
b1,
b2,
b3,
b4 being
Element of
for
M,
N being
Subset of st
M _|_ N &
a1 in M &
a3 in M &
b1 in M &
b3 in M &
a2 in N &
a4 in N &
b2 in N &
b4 in N & not
a2 in M & not
a4 in M &
a1,
a2 _|_ b1,
b2 &
a2,
a3 _|_ b2,
b3 &
a3,
a4 _|_ b3,
b4 holds
a1,
a4 _|_ b1,
b4;
attr X is
satisfying_MH2 means :
Def4:
for
a1,
a2,
a3,
a4,
b1,
b2,
b3,
b4 being
Element of
for
M,
N being
Subset of st
M _|_ N &
a1 in M &
a3 in M &
b2 in M &
b4 in M &
a2 in N &
a4 in N &
b1 in N &
b3 in N & not
a2 in M & not
a4 in M &
a1,
a2 _|_ b1,
b2 &
a2,
a3 _|_ b2,
b3 &
a3,
a4 _|_ b3,
b4 holds
a1,
a4 _|_ b1,
b4;
attr X is
satisfying_TDES means :
Def5:
for
o,
a,
a1,
b,
b1,
c,
c1 being
Element of st
o <> a &
o <> a1 &
o <> b &
o <> b1 &
o <> c &
o <> c1 & not
LIN b,
b1,
a & not
LIN b,
b1,
c &
LIN o,
a,
a1 &
LIN o,
b,
b1 &
LIN o,
c,
c1 &
a,
b // a1,
b1 &
a,
b // o,
c &
b,
c // b1,
c1 holds
a,
c // a1,
c1;
attr X is
satisfying_SCH means
for
a1,
a2,
a3,
a4,
b1,
b2,
b3,
b4 being
Element of
for
M,
N being
Subset of st
M is
being_line &
N is
being_line &
a1 in M &
a3 in M &
b1 in M &
b3 in M &
a2 in N &
a4 in N &
b2 in N &
b4 in N & not
a4 in M & not
a2 in M & not
b2 in M & not
b4 in M & not
a1 in N & not
a3 in N & not
b1 in N & not
b3 in N &
a3,
a2 // b3,
b2 &
a2,
a1 // b2,
b1 &
a1,
a4 // b1,
b4 holds
a3,
a4 // b3,
b4;
attr X is
satisfying_OSCH means :
Def7:
for
a1,
a2,
a3,
a4,
b1,
b2,
b3,
b4 being
Element of
for
M,
N being
Subset of st
M _|_ N &
a1 in M &
a3 in M &
b1 in M &
b3 in M &
a2 in N &
a4 in N &
b2 in N &
b4 in N & not
a4 in M & not
a2 in M & not
b2 in M & not
b4 in M & not
a1 in N & not
a3 in N & not
b1 in N & not
b3 in N &
a3,
a2 // b3,
b2 &
a2,
a1 // b2,
b1 &
a1,
a4 // b1,
b4 holds
a3,
a4 // b3,
b4;
attr X is
satisfying_des means :
Def8:
for
a,
a1,
b,
b1,
c,
c1 being
Element of st not
LIN a,
a1,
b & not
LIN a,
a1,
c &
a,
a1 // b,
b1 &
a,
a1 // c,
c1 &
a,
b // a1,
b1 &
a,
c // a1,
c1 holds
b,
c // b1,
c1;
end;
:: deftheorem Def1 defines satisfying_OPAP CONMETR:def 1 :
for
X being
OrtAfPl holds
(
X is
satisfying_OPAP iff for
o,
a1,
a2,
a3,
b1,
b2,
b3 being
Element of
for
M,
N being
Subset of st
o in M &
a1 in M &
a2 in M &
a3 in M &
o in N &
b1 in N &
b2 in N &
b3 in N & not
b2 in M & not
a3 in N &
M _|_ N &
o <> a1 &
o <> a2 &
o <> a3 &
o <> b1 &
o <> b2 &
o <> b3 &
a3,
b2 // a2,
b1 &
a3,
b3 // a1,
b1 holds
a1,
b2 // a2,
b3 );
:: deftheorem defines satisfying_PAP CONMETR:def 2 :
for
X being
OrtAfPl holds
(
X is
satisfying_PAP iff for
o,
a1,
a2,
a3,
b1,
b2,
b3 being
Element of
for
M,
N being
Subset of st
M is
being_line &
N is
being_line &
o in M &
a1 in M &
a2 in M &
a3 in M &
o in N &
b1 in N &
b2 in N &
b3 in N & not
b2 in M & not
a3 in N &
o <> a1 &
o <> a2 &
o <> a3 &
o <> b1 &
o <> b2 &
o <> b3 &
a3,
b2 // a2,
b1 &
a3,
b3 // a1,
b1 holds
a1,
b2 // a2,
b3 );
:: deftheorem Def3 defines satisfying_MH1 CONMETR:def 3 :
for
X being
OrtAfPl holds
(
X is
satisfying_MH1 iff for
a1,
a2,
a3,
a4,
b1,
b2,
b3,
b4 being
Element of
for
M,
N being
Subset of st
M _|_ N &
a1 in M &
a3 in M &
b1 in M &
b3 in M &
a2 in N &
a4 in N &
b2 in N &
b4 in N & not
a2 in M & not
a4 in M &
a1,
a2 _|_ b1,
b2 &
a2,
a3 _|_ b2,
b3 &
a3,
a4 _|_ b3,
b4 holds
a1,
a4 _|_ b1,
b4 );
:: deftheorem Def4 defines satisfying_MH2 CONMETR:def 4 :
for
X being
OrtAfPl holds
(
X is
satisfying_MH2 iff for
a1,
a2,
a3,
a4,
b1,
b2,
b3,
b4 being
Element of
for
M,
N being
Subset of st
M _|_ N &
a1 in M &
a3 in M &
b2 in M &
b4 in M &
a2 in N &
a4 in N &
b1 in N &
b3 in N & not
a2 in M & not
a4 in M &
a1,
a2 _|_ b1,
b2 &
a2,
a3 _|_ b2,
b3 &
a3,
a4 _|_ b3,
b4 holds
a1,
a4 _|_ b1,
b4 );
:: deftheorem Def5 defines satisfying_TDES CONMETR:def 5 :
for
X being
OrtAfPl holds
(
X is
satisfying_TDES iff for
o,
a,
a1,
b,
b1,
c,
c1 being
Element of st
o <> a &
o <> a1 &
o <> b &
o <> b1 &
o <> c &
o <> c1 & not
LIN b,
b1,
a & not
LIN b,
b1,
c &
LIN o,
a,
a1 &
LIN o,
b,
b1 &
LIN o,
c,
c1 &
a,
b // a1,
b1 &
a,
b // o,
c &
b,
c // b1,
c1 holds
a,
c // a1,
c1 );
:: deftheorem defines satisfying_SCH CONMETR:def 6 :
for
X being
OrtAfPl holds
(
X is
satisfying_SCH iff for
a1,
a2,
a3,
a4,
b1,
b2,
b3,
b4 being
Element of
for
M,
N being
Subset of st
M is
being_line &
N is
being_line &
a1 in M &
a3 in M &
b1 in M &
b3 in M &
a2 in N &
a4 in N &
b2 in N &
b4 in N & not
a4 in M & not
a2 in M & not
b2 in M & not
b4 in M & not
a1 in N & not
a3 in N & not
b1 in N & not
b3 in N &
a3,
a2 // b3,
b2 &
a2,
a1 // b2,
b1 &
a1,
a4 // b1,
b4 holds
a3,
a4 // b3,
b4 );
:: deftheorem Def7 defines satisfying_OSCH CONMETR:def 7 :
for
X being
OrtAfPl holds
(
X is
satisfying_OSCH iff for
a1,
a2,
a3,
a4,
b1,
b2,
b3,
b4 being
Element of
for
M,
N being
Subset of st
M _|_ N &
a1 in M &
a3 in M &
b1 in M &
b3 in M &
a2 in N &
a4 in N &
b2 in N &
b4 in N & not
a4 in M & not
a2 in M & not
b2 in M & not
b4 in M & not
a1 in N & not
a3 in N & not
b1 in N & not
b3 in N &
a3,
a2 // b3,
b2 &
a2,
a1 // b2,
b1 &
a1,
a4 // b1,
b4 holds
a3,
a4 // b3,
b4 );
:: deftheorem Def8 defines satisfying_des CONMETR:def 8 :
for
X being
OrtAfPl holds
(
X is
satisfying_des iff for
a,
a1,
b,
b1,
c,
c1 being
Element of st not
LIN a,
a1,
b & not
LIN a,
a1,
c &
a,
a1 // b,
b1 &
a,
a1 // c,
c1 &
a,
b // a1,
b1 &
a,
c // a1,
c1 holds
b,
c // b1,
c1 );
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem
theorem
theorem
theorem
theorem
theorem
theorem