begin
definition
let AP be
AffinPlane;
attr AP is
satisfying_DES1 means :
Def1:
for
A,
P,
C being
Subset of
AP for
o,
a,
a',
b,
b',
c,
c',
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 &
a' in A &
o in P &
b in P &
b' in P &
o in C &
c in C &
c' in C &
o <> a &
o <> b &
o <> c &
p <> q & not
LIN b,
a,
c & not
LIN b',
a',
c' &
a <> a' &
LIN b,
a,
p &
LIN b',
a',
p &
LIN b,
c,
q &
LIN b',
c',
q &
a,
c // a',
c' 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,
a',
b,
b',
c,
c',
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 &
a' in A &
o in P &
b in P &
b' in P &
o in C &
c in C &
c' in C &
o <> a &
o <> b &
o <> c &
p <> q & not
LIN b,
a,
c & not
LIN b',
a',
c' &
a <> a' &
LIN b,
a,
p &
LIN b',
a',
p &
LIN b,
c,
q &
LIN b',
c',
q &
a,
c // a',
c' 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,
a',
b,
b',
c,
c',
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 &
a' in A &
o in P &
b in P &
b' in P &
o in C &
c in C &
c' in C &
o <> a &
o <> b &
o <> c &
p <> q &
c <> q & not
LIN b,
a,
c & not
LIN b',
a',
c' &
LIN b,
a,
p &
LIN b',
a',
p &
LIN b,
c,
q &
LIN b',
c',
q &
a,
c // p,
q holds
a,
c // a',
c';
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,
a',
b,
b',
c,
c',
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 &
a' in A &
o in P &
b in P &
b' in P &
o in C &
c in C &
c' in C &
o <> a &
o <> b &
o <> c &
p <> q &
c <> q & not
LIN b,
a,
c & not
LIN b',
a',
c' &
LIN b,
a,
p &
LIN b',
a',
p &
LIN b,
c,
q &
LIN b',
c',
q &
a,
c // p,
q holds
a,
c // a',
c' );
definition
let AP be
AffinPlane;
attr AP is
satisfying_DES1_2 means :
Def3:
for
A,
P,
C being
Subset of
AP for
o,
a,
a',
b,
b',
c,
c',
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 &
a' in A &
o in P &
b in P &
b' in P &
c in C &
c' in C &
o <> a &
o <> b &
o <> c &
p <> q & not
LIN b,
a,
c & not
LIN b',
a',
c' &
c <> c' &
LIN b,
a,
p &
LIN b',
a',
p &
LIN b,
c,
q &
LIN b',
c',
q &
a,
c // a',
c' &
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,
a',
b,
b',
c,
c',
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 &
a' in A &
o in P &
b in P &
b' in P &
c in C &
c' in C &
o <> a &
o <> b &
o <> c &
p <> q & not
LIN b,
a,
c & not
LIN b',
a',
c' &
c <> c' &
LIN b,
a,
p &
LIN b',
a',
p &
LIN b,
c,
q &
LIN b',
c',
q &
a,
c // a',
c' &
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,
a',
b,
b',
c,
c',
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 &
a' in A &
b in P &
b' in P &
o in C &
c in C &
c' in C &
o <> a &
o <> b &
o <> c &
p <> q & not
LIN b,
a,
c & not
LIN b',
a',
c' &
b <> b' &
a <> a' &
LIN b,
a,
p &
LIN b',
a',
p &
LIN b,
c,
q &
LIN b',
c',
q &
a,
c // a',
c' &
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,
a',
b,
b',
c,
c',
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 &
a' in A &
b in P &
b' in P &
o in C &
c in C &
c' in C &
o <> a &
o <> b &
o <> c &
p <> q & not
LIN b,
a,
c & not
LIN b',
a',
c' &
b <> b' &
a <> a' &
LIN b,
a,
p &
LIN b',
a',
p &
LIN b,
c,
q &
LIN b',
c',
q &
a,
c // a',
c' &
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,
a',
b,
b',
c,
c',
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 &
a' in A &
b in P &
b' in P &
c in C &
c' in C &
A // P &
A // C & not
LIN b,
a,
c & not
LIN b',
a',
c' &
p <> q &
a <> a' &
LIN b,
a,
p &
LIN b',
a',
p &
LIN b,
c,
q &
LIN b',
c',
q &
a,
c // a',
c' 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,
a',
b,
b',
c,
c',
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 &
a' in A &
b in P &
b' in P &
c in C &
c' in C &
A // P &
A // C & not
LIN b,
a,
c & not
LIN b',
a',
c' &
p <> q &
a <> a' &
LIN b,
a,
p &
LIN b',
a',
p &
LIN b,
c,
q &
LIN b',
c',
q &
a,
c // a',
c' 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,
a',
b,
b',
c,
c',
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 &
a' in A &
b in P &
b' in P &
c in C &
c' in C &
A // P &
A // C & not
LIN b,
a,
c & not
LIN b',
a',
c' &
p <> q &
LIN b,
a,
p &
LIN b',
a',
p &
LIN b,
c,
q &
LIN b',
c',
q &
a,
c // p,
q holds
a,
c // a',
c';
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,
a',
b,
b',
c,
c',
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 &
a' in A &
b in P &
b' in P &
c in C &
c' in C &
A // P &
A // C & not
LIN b,
a,
c & not
LIN b',
a',
c' &
p <> q &
LIN b,
a,
p &
LIN b',
a',
p &
LIN b,
c,
q &
LIN b',
c',
q &
a,
c // p,
q holds
a,
c // a',
c' );
definition
let AP be
AffinPlane;
attr AP is
satisfying_DES2_2 means :
Def7:
for
A,
P,
C being
Subset of
AP for
a,
a',
b,
b',
c,
c',
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 &
a' in A &
b in P &
b' in P &
c in C &
c' in C &
A // C & not
LIN b,
a,
c & not
LIN b',
a',
c' &
p <> q &
a <> a' &
LIN b,
a,
p &
LIN b',
a',
p &
LIN b,
c,
q &
LIN b',
c',
q &
a,
c // a',
c' &
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,
a',
b,
b',
c,
c',
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 &
a' in A &
b in P &
b' in P &
c in C &
c' in C &
A // C & not
LIN b,
a,
c & not
LIN b',
a',
c' &
p <> q &
a <> a' &
LIN b,
a,
p &
LIN b',
a',
p &
LIN b,
c,
q &
LIN b',
c',
q &
a,
c // a',
c' &
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,
a',
b,
b',
c,
c',
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 &
a' in A &
b in P &
b' in P &
c in C &
c' in C &
A // P & not
LIN b,
a,
c & not
LIN b',
a',
c' &
p <> q &
c <> c' &
LIN b,
a,
p &
LIN b',
a',
p &
LIN b,
c,
q &
LIN b',
c',
q &
a,
c // a',
c' &
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,
a',
b,
b',
c,
c',
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 &
a' in A &
b in P &
b' in P &
c in C &
c' in C &
A // P & not
LIN b,
a,
c & not
LIN b',
a',
c' &
p <> q &
c <> c' &
LIN b,
a,
p &
LIN b',
a',
p &
LIN b,
c,
q &
LIN b',
c',
q &
a,
c // a',
c' &
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