:: by Eugeniusz Kusak, Henryk Oryszczyszyn and Krzysztof Pra\.zmowski

::

:: Received April 26, 1990

:: Copyright (c) 1990-2018 Association of Mizar Users

definition

let AP be AffinPlane;

end;
attr AP is satisfying_DES1 means :: AFF_3:def 1

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;

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;

:: deftheorem 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 );

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;

end;
attr AP is satisfying_DES1_1 means :: AFF_3:def 2

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;

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;

:: deftheorem 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 );

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;

end;
attr AP is satisfying_DES1_2 means :: AFF_3:def 3

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;

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;

:: deftheorem 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 );

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;

end;
attr AP is satisfying_DES1_3 means :: AFF_3:def 4

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;

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;

:: deftheorem 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 );

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;

end;
attr AP is satisfying_DES2 means :: AFF_3:def 5

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;

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;

:: deftheorem 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 );

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;

end;
attr AP is satisfying_DES2_1 means :: AFF_3:def 6

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;

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;

:: deftheorem 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 );

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;

end;
attr AP is satisfying_DES2_2 means :: AFF_3:def 7

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;

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;

:: deftheorem 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 );

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;

end;
attr AP is satisfying_DES2_3 means :: AFF_3:def 8

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;

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;

:: deftheorem 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 );

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 );