begin
definition
let AP be
AffinPlane;
attr AP is
satisfying_DES1 means :
Def1:
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:
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:
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:
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:
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:
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:
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:
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
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem