:: PAPDESAF semantic presentation

begin

registration
let OAS be OAffinSpace;
cluster Lambda OAS ->  non trivial AffinSpace-like ;
correctness
coherence
( Lambda OAS is AffinSpace-like & not Lambda OAS is trivial );
by DIRAF:41;
end;

registration
let OAS be OAffinPlane;
cluster Lambda OAS ->  2-dimensional ;
correctness
coherence
Lambda OAS is 2-dimensional ;
by DIRAF:45;
end;

theorem Th1: :: PAPDESAF:1
for OAS being OAffinSpace
for x being set holds
( ( x is Element of OAS implies x is Element of (Lambda OAS) ) & ( x is Element of (Lambda OAS) implies x is Element of OAS ) & ( x is Subset of OAS implies x is Subset of (Lambda OAS) ) & ( x is Subset of (Lambda OAS) implies x is Subset of OAS ) )
proof
let OAS be OAffinSpace; ::_thesis: for x being set holds
( ( x is Element of OAS implies x is Element of (Lambda OAS) ) & ( x is Element of (Lambda OAS) implies x is Element of OAS ) & ( x is Subset of OAS implies x is Subset of (Lambda OAS) ) & ( x is Subset of (Lambda OAS) implies x is Subset of OAS ) )
 Lambda OAS = AffinStruct(# the carrier of OAS,(lambda the CONGR of OAS) #) by DIRAF:def_2;
hence  for x being set holds
( ( x is Element of OAS implies x is Element of (Lambda OAS) ) & ( x is Element of (Lambda OAS) implies x is Element of OAS ) & ( x is Subset of OAS implies x is Subset of (Lambda OAS) ) & ( x is Subset of (Lambda OAS) implies x is Subset of OAS ) ) ; ::_thesis: verum
end;

theorem Th2: :: PAPDESAF:2
for OAS being OAffinSpace
for a, b, c being Element of OAS
for a9, b9, c9 being Element of (Lambda OAS) st a = a9 & b = b9 & c = c9 holds
( LIN a,b,c iff LIN a9,b9,c9 )
proof
let OAS be OAffinSpace; ::_thesis: for a, b, c being Element of OAS
for a9, b9, c9 being Element of (Lambda OAS) st a = a9 & b = b9 & c = c9 holds
( LIN a,b,c iff LIN a9,b9,c9 )
let a, b, c be Element of OAS; ::_thesis: for a9, b9, c9 being Element of (Lambda OAS) st a = a9 & b = b9 & c = c9 holds
( LIN a,b,c iff LIN a9,b9,c9 )
let a9, b9, c9 be Element of (Lambda OAS); ::_thesis: ( a = a9 & b = b9 & c = c9 implies ( LIN a,b,c iff LIN a9,b9,c9 ) )
assume A1: ( a = a9 & b = b9 & c = c9 ) ; ::_thesis: ( LIN a,b,c iff LIN a9,b9,c9 )
A2: now__::_thesis:_(_LIN_a,b,c_implies_LIN_a9,b9,c9_)
assume  LIN a,b,c ; ::_thesis: LIN a9,b9,c9
then  a,b '||' a,c by DIRAF:def_5;
then  a9,b9 // a9,c9 by A1, DIRAF:38;
hence  LIN a9,b9,c9 by AFF_1:def_1; ::_thesis: verum
end;
now__::_thesis:_(_LIN_a9,b9,c9_implies_LIN_a,b,c_)
assume  LIN a9,b9,c9 ; ::_thesis: LIN a,b,c
then  a9,b9 // a9,c9 by AFF_1:def_1;
then  a,b '||' a,c by A1, DIRAF:38;
hence  LIN a,b,c by DIRAF:def_5; ::_thesis: verum
end;
hence  ( LIN a,b,c iff LIN a9,b9,c9 ) by A2; ::_thesis: verum
end;

theorem Th3: :: PAPDESAF:3
for V being RealLinearSpace
for x being set holds
( x is Element of (OASpace V) iff x is VECTOR of V )
proof
let V be RealLinearSpace; ::_thesis: for x being set holds
( x is Element of (OASpace V) iff x is VECTOR of V )
let x be set ; ::_thesis: ( x is Element of (OASpace V) iff x is VECTOR of V )
 OASpace V = AffinStruct(# the carrier of V,(DirPar V) #) by ANALOAF:def_4;
hence  ( x is Element of (OASpace V) iff x is VECTOR of V ) ; ::_thesis: verum
end;

theorem Th4: :: PAPDESAF:4
for V being RealLinearSpace
for OAS being OAffinSpace st OAS = OASpace V holds
for a, b, c, d being Element of OAS
for u, v, w, y being VECTOR of V st a = u & b = v & c = w & d = y holds
( a,b '||' c,d iff u,v '||' w,y )
proof
let V be RealLinearSpace; ::_thesis: for OAS being OAffinSpace st OAS = OASpace V holds
for a, b, c, d being Element of OAS
for u, v, w, y being VECTOR of V st a = u & b = v & c = w & d = y holds
( a,b '||' c,d iff u,v '||' w,y )
let OAS be OAffinSpace; ::_thesis: ( OAS = OASpace V implies for a, b, c, d being Element of OAS
for u, v, w, y being VECTOR of V st a = u & b = v & c = w & d = y holds
( a,b '||' c,d iff u,v '||' w,y ) )
assume A1: OAS = OASpace V ; ::_thesis: for a, b, c, d being Element of OAS
for u, v, w, y being VECTOR of V st a = u & b = v & c = w & d = y holds
( a,b '||' c,d iff u,v '||' w,y )
let a, b, c, d be Element of OAS; ::_thesis: for u, v, w, y being VECTOR of V st a = u & b = v & c = w & d = y holds
( a,b '||' c,d iff u,v '||' w,y )
let u, v, w, y be VECTOR of V; ::_thesis: ( a = u & b = v & c = w & d = y implies ( a,b '||' c,d iff u,v '||' w,y ) )
assume A2: ( a = u & b = v & c = w & d = y ) ; ::_thesis: ( a,b '||' c,d iff u,v '||' w,y )
A3: now__::_thesis:_(_u,v_'||'_w,y_implies_a,b_'||'_c,d_)
assume  u,v '||' w,y ; ::_thesis: a,b '||' c,d
then  ( u,v // w,y or u,v // y,w ) by GEOMTRAP:def_1;
then  ( a,b // c,d or a,b // d,c ) by A1, A2, GEOMTRAP:2;
hence  a,b '||' c,d by DIRAF:def_4; ::_thesis: verum
end;
now__::_thesis:_(_a,b_'||'_c,d_implies_u,v_'||'_w,y_)
assume  a,b '||' c,d ; ::_thesis: u,v '||' w,y
then  ( a,b // c,d or a,b // d,c ) by DIRAF:def_4;
then  ( u,v // w,y or u,v // y,w ) by A1, A2, GEOMTRAP:2;
hence  u,v '||' w,y by GEOMTRAP:def_1; ::_thesis: verum
end;
hence  ( a,b '||' c,d iff u,v '||' w,y ) by A3; ::_thesis: verum
end;

theorem :: PAPDESAF:5
for V being RealLinearSpace
for OAS being OAffinSpace st OAS = OASpace V holds
ex u, v being VECTOR of V st
for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 )
proof
let V be RealLinearSpace; ::_thesis: for OAS being OAffinSpace st OAS = OASpace V holds
ex u, v being VECTOR of V st
for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 )
let OAS be OAffinSpace; ::_thesis: ( OAS = OASpace V implies ex u, v being VECTOR of V st
for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) )
assume A1: OAS = OASpace V ; ::_thesis: ex u, v being VECTOR of V st
for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 )
consider a, b, c, d being Element of OAS such that
A2: ( not a,b // c,d & not a,b // d,c ) by ANALOAF:def_5;
reconsider u = a, v = b, w = c, y = d as VECTOR of V by A1, Th3;
take z1 = v - u; ::_thesis: ex v being VECTOR of V st
for a, b being Real st (a * z1) + (b * v) = 0. V holds
( a = 0 & b = 0 )
take z2 = y - w; ::_thesis: for a, b being Real st (a * z1) + (b * z2) = 0. V holds
( a = 0 & b = 0 )
now__::_thesis:_for_r1,_r2_being_Real_st_(r1_*_z1)_+_(r2_*_z2)_=_0._V_&_(_r1_<>_0_or_r2_<>_0_)_holds_
(_r1_=_0_&_r2_=_0_)
let r1, r2 be Real; ::_thesis: ( (r1 * z1) + (r2 * z2) = 0. V & ( r1 <> 0 or r2 <> 0 ) implies ( r1 = 0 & r2 = 0 ) )
assume  (r1 * z1) + (r2 * z2) = 0. V ; ::_thesis: ( ( r1 <> 0 or r2 <> 0 ) implies ( r1 = 0 & r2 = 0 ) )
then A3: r1 * z1 = - (r2 * z2) by RLVECT_1:6
.= r2 * (- z2) by RLVECT_1:25
.= (- r2) * z2 by RLVECT_1:24 ;
assume  ( r1 <> 0 or r2 <> 0 ) ; ::_thesis: ( r1 = 0 & r2 = 0 )
then  ( r1 <> 0 or - r2 <> 0 ) ;
then  ( u,v // w,y or u,v // y,w ) by A3, ANALMETR:14;
hence  ( r1 = 0 & r2 = 0 ) by A1, A2, GEOMTRAP:2; ::_thesis: verum
end;
hence  for a, b being Real st (a * z1) + (b * z2) = 0. V holds
( a = 0 & b = 0 ) ; ::_thesis: verum
end;

definition
let AS be AffinSpace;
redefine attr AS is Fanoian  means :Def1: :: PAPDESAF:def 1
 for a, b, c, d being Element of AS st a,b // c,d & a,c // b,d & a,d // b,c holds
a,b // a,c;
compatibility
 ( AS is Fanoian iff for a, b, c, d being Element of AS st a,b // c,d & a,c // b,d & a,d // b,c holds
a,b // a,c )
proof
thus  ( AS is Fanoian implies for a, b, c, d being Element of AS st a,b // c,d & a,c // b,d & a,d // b,c holds
a,b // a,c ) ::_thesis: ( ( for a, b, c, d being Element of AS st a,b // c,d & a,c // b,d & a,d // b,c holds
a,b // a,c ) implies AS is Fanoian )
proof
assume A1: for a, b, c, d being Element of AS st a,b // c,d & a,c // b,d & a,d // b,c holds
LIN a,b,c ; :: according to TRANSLAC:def_1 ::_thesis: for a, b, c, d being Element of AS st a,b // c,d & a,c // b,d & a,d // b,c holds
a,b // a,c
let a, b, c, d be Element of AS; ::_thesis: ( a,b // c,d & a,c // b,d & a,d // b,c implies a,b // a,c )
assume  ( a,b // c,d & a,c // b,d & a,d // b,c ) ; ::_thesis: a,b // a,c
then  LIN a,b,c by A1;
hence  a,b // a,c by AFF_1:def_1; ::_thesis: verum
end;
assume A2: for a, b, c, d being Element of AS st a,b // c,d & a,c // b,d & a,d // b,c holds
a,b // a,c ; ::_thesis: AS is Fanoian
let a, b, c, d be Element of AS; :: according to TRANSLAC:def_1 ::_thesis: ( not a,b // c,d or not a,c // b,d or not a,d // b,c or LIN a,b,c )
assume  ( a,b // c,d & a,c // b,d & a,d // b,c ) ; ::_thesis: LIN a,b,c
then  a,b // a,c by A2;
hence  LIN a,b,c by AFF_1:def_1; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines Fanoian PAPDESAF:def_1_:_
 for AS being AffinSpace holds
( AS is Fanoian iff for a, b, c, d being Element of AS st a,b // c,d & a,c // b,d & a,d // b,c holds
a,b // a,c );

definition
let IT be OAffinSpace;
attrIT is Pappian  means :Def2: :: PAPDESAF:def 2
 Lambda IT is Pappian ;
attrIT is Desarguesian  means :Def3: :: PAPDESAF:def 3
 Lambda IT is Desarguesian ;
attrIT is Moufangian  means :Def4: :: PAPDESAF:def 4
 Lambda IT is Moufangian ;
attrIT is translation  means :Def5: :: PAPDESAF:def 5
 Lambda IT is translational ;
end;

:: deftheorem Def2 defines Pappian PAPDESAF:def_2_:_
 for IT being OAffinSpace holds
( IT is Pappian iff Lambda IT is Pappian );

:: deftheorem Def3 defines Desarguesian PAPDESAF:def_3_:_
 for IT being OAffinSpace holds
( IT is Desarguesian iff Lambda IT is Desarguesian );

:: deftheorem Def4 defines Moufangian PAPDESAF:def_4_:_
 for IT being OAffinSpace holds
( IT is Moufangian iff Lambda IT is Moufangian );

:: deftheorem Def5 defines translation PAPDESAF:def_5_:_
 for IT being OAffinSpace holds
( IT is translation iff Lambda IT is translational );

definition
let OAS be OAffinSpace;
attrOAS is satisfying_DES  means :Def6: :: PAPDESAF:def 6
 for o, a, b, c, a1, b1, c1 being Element of OAS st o,a // o,a1 & o,b // o,b1 & o,c // o,c1 & not LIN o,a,b & not LIN o,a,c & a,b // a1,b1 & a,c // a1,c1 holds
b,c // b1,c1;
end;

:: deftheorem Def6 defines satisfying_DES PAPDESAF:def_6_:_
 for OAS being OAffinSpace holds
( OAS is satisfying_DES iff for o, a, b, c, a1, b1, c1 being Element of OAS st o,a // o,a1 & o,b // o,b1 & o,c // o,c1 & not LIN o,a,b & not LIN o,a,c & a,b // a1,b1 & a,c // a1,c1 holds
b,c // b1,c1 );

definition
let OAS be OAffinSpace;
attrOAS is satisfying_DES_1  means :Def7: :: PAPDESAF:def 7
 for o, a, b, c, a1, b1, c1 being Element of OAS st a,o // o,a1 & b,o // o,b1 & c,o // o,c1 & not LIN o,a,b & not LIN o,a,c & a,b // b1,a1 & a,c // c1,a1 holds
b,c // c1,b1;
end;

:: deftheorem Def7 defines satisfying_DES_1 PAPDESAF:def_7_:_
 for OAS being OAffinSpace holds
( OAS is satisfying_DES_1 iff for o, a, b, c, a1, b1, c1 being Element of OAS st a,o // o,a1 & b,o // o,b1 & c,o // o,c1 & not LIN o,a,b & not LIN o,a,c & a,b // b1,a1 & a,c // c1,a1 holds
b,c // c1,b1 );

theorem Th6: :: PAPDESAF:6
for OAS being OAffinSpace st OAS is satisfying_DES_1 holds
OAS is satisfying_DES
proof
let OAS be OAffinSpace; ::_thesis: ( OAS is satisfying_DES_1 implies OAS is satisfying_DES )
assume A1: OAS is satisfying_DES_1 ; ::_thesis: OAS is satisfying_DES
 for o, a, b, c, a1, b1, c1 being Element of OAS st o,a // o,a1 & o,b // o,b1 & o,c // o,c1 & not LIN o,a,b & not LIN o,a,c & a,b // a1,b1 & a,c // a1,c1 holds
b,c // b1,c1
proof
let o, a, b, c, a1, b1, c1 be Element of OAS; ::_thesis: ( o,a // o,a1 & o,b // o,b1 & o,c // o,c1 & not LIN o,a,b & not LIN o,a,c & a,b // a1,b1 & a,c // a1,c1 implies b,c // b1,c1 )
assume that
A2: o,a // o,a1 and
A3: o,b // o,b1 and
A4: o,c // o,c1 and
A5: not LIN o,a,b and
A6: not LIN o,a,c and
A7: a,b // a1,b1 and
A8: a,c // a1,c1 ; ::_thesis: b,c // b1,c1
consider a2 being Element of OAS such that
A9: Mid a,o,a2 and
A10: o <> a2 by DIRAF:13;
A11: a,o // o,a2 by A9, DIRAF:def_3;
A12: o <> a by A5, DIRAF:31;
then consider c2 being Element of OAS such that
A13: c,o // o,c2 and
A14: c,a // a2,c2 by A11, ANALOAF:def_5;
A15: c2,a2 // a,c by A14, DIRAF:2;
A16: c2,o // o,c by A13, DIRAF:2;
then  Mid c2,o,c by DIRAF:def_3;
then A17: LIN c2,o,c by DIRAF:28;
 LIN a,o,a2 by A9, DIRAF:28;
then A18: LIN o,a2,a by DIRAF:30;
A19: o <> c2
proof
assume  o = c2 ; ::_thesis: contradiction
then  o,a2 // a,c by A14, DIRAF:2;
then  o,a2 '||' a,c by DIRAF:def_4;
then  ( LIN o,a2,o & LIN o,a2,c ) by A10, A18, DIRAF:31, DIRAF:33;
hence  contradiction by A6, A10, A18, DIRAF:32; ::_thesis: verum
end;
A20: not LIN o,a2,c2
proof
A21: LIN c2,o,o by DIRAF:31;
A22: LIN o,a2,o by DIRAF:31;
assume  LIN o,a2,c2 ; ::_thesis: contradiction
then  LIN c2,o,a by A10, A18, A22, DIRAF:32;
hence  contradiction by A6, A17, A19, A21, DIRAF:32; ::_thesis: verum
end;
consider b2 being Element of OAS such that
A23: b,o // o,b2 and
A24: b,a // a2,b2 by A12, A11, ANALOAF:def_5;
A25: b2,a2 // a,b by A24, DIRAF:2;
 a <> b by A5, DIRAF:31;
then  b2,a2 // a1,b1 by A7, A25, DIRAF:3;
then A26: a2,b2 // b1,a1 by DIRAF:2;
 o <> c by A6, DIRAF:31;
then A27: c2,o // o,c1 by A4, A16, DIRAF:3;
A28: a,c // c2,a2 by A14, ANALOAF:def_5;
A29: b2,o // o,b by A23, DIRAF:2;
then  Mid b2,o,b by DIRAF:def_3;
then A30: LIN b2,o,b by DIRAF:28;
A31: o <> b2
proof
assume  o = b2 ; ::_thesis: contradiction
then  o,a2 // a,b by A24, DIRAF:2;
then  o,a2 '||' a,b by DIRAF:def_4;
then  ( LIN o,a2,o & LIN o,a2,b ) by A10, A18, DIRAF:31, DIRAF:33;
hence  contradiction by A5, A10, A18, DIRAF:32; ::_thesis: verum
end;
A32: not LIN o,a2,b2
proof
A33: LIN b2,o,o by DIRAF:31;
A34: LIN o,a2,o by DIRAF:31;
assume  LIN o,a2,b2 ; ::_thesis: contradiction
then  LIN b2,o,a by A10, A18, A34, DIRAF:32;
hence  contradiction by A5, A30, A31, A33, DIRAF:32; ::_thesis: verum
end;
A35: now__::_thesis:_(_c2_=_b2_implies_b,c_//_b1,c1_)
 b2,a2 // a,b by A24, DIRAF:2;
then A36: b2,a2 '||' a,b by DIRAF:def_4;
assume A37: c2 = b2 ; ::_thesis: b,c // b1,c1
then A38: LIN o,b2,c by A17, DIRAF:30;
 c2,a2 // a,c by A14, DIRAF:2;
then A39: b2,a2 '||' a,c by A37, DIRAF:def_4;
 ( not LIN o,b2,a2 & LIN o,b2,b ) by A30, A32, DIRAF:30;
then  b = c by A18, A38, A36, A39, PASCH:4;
hence  b,c // b1,c1 by DIRAF:4; ::_thesis: verum
end;
 a2,o // o,a by A11, DIRAF:2;
then A40: a2,o // o,a1 by A2, A12, DIRAF:3;
 a <> c by A6, DIRAF:31;
then  c2,a2 // a1,c1 by A8, A15, DIRAF:3;
then A41: a2,c2 // c1,a1 by DIRAF:2;
 o <> b by A5, DIRAF:31;
then  b2,o // o,b1 by A3, A29, DIRAF:3;
then A42: c2,b2 // b1,c1 by A1, A40, A27, A41, A26, A32, A20, Def7;
 a,b // b2,a2 by A24, ANALOAF:def_5;
then  b,c // c2,b2 by A1, A5, A6, A11, A23, A13, A28, Def7;
hence  b,c // b1,c1 by A42, A35, DIRAF:3; ::_thesis: verum
end;
hence  OAS is satisfying_DES by Def6; ::_thesis: verum
end;

theorem Th7: :: PAPDESAF:7
for OAS being OAffinSpace
for o, a, b, a9, b9 being Element of OAS st not LIN o,a,b & a,o // o,a9 & LIN o,b,b9 & a,b '||' a9,b9 holds
( b,o // o,b9 & a,b // b9,a9 )
proof
let OAS be OAffinSpace; ::_thesis: for o, a, b, a9, b9 being Element of OAS st not LIN o,a,b & a,o // o,a9 & LIN o,b,b9 & a,b '||' a9,b9 holds
( b,o // o,b9 & a,b // b9,a9 )
let o, a, b, a9, b9 be Element of OAS; ::_thesis: ( not LIN o,a,b & a,o // o,a9 & LIN o,b,b9 & a,b '||' a9,b9 implies ( b,o // o,b9 & a,b // b9,a9 ) )
assume that
A1: not LIN o,a,b and
A2: a,o // o,a9 and
A3: LIN o,b,b9 and
A4: a,b '||' a9,b9 ; ::_thesis: ( b,o // o,b9 & a,b // b9,a9 )
 ( Mid a,o,a9 & a,b '||' b9,a9 ) by A2, A4, DIRAF:22, DIRAF:def_3;
then  Mid b,o,b9 by A1, A3, PASCH:6;
hence  b,o // o,b9 by DIRAF:def_3; ::_thesis: a,b // b9,a9
hence  a,b // b9,a9 by A1, A2, A4, PASCH:12; ::_thesis: verum
end;

theorem Th8: :: PAPDESAF:8
for OAS being OAffinSpace
for o, a, b, a9, b9 being Element of OAS st not LIN o,a,b & o,a // o,a9 & LIN o,b,b9 & a,b '||' a9,b9 holds
( o,b // o,b9 & a,b // a9,b9 )
proof
let OAS be OAffinSpace; ::_thesis: for o, a, b, a9, b9 being Element of OAS st not LIN o,a,b & o,a // o,a9 & LIN o,b,b9 & a,b '||' a9,b9 holds
( o,b // o,b9 & a,b // a9,b9 )
let o, a, b, a9, b9 be Element of OAS; ::_thesis: ( not LIN o,a,b & o,a // o,a9 & LIN o,b,b9 & a,b '||' a9,b9 implies ( o,b // o,b9 & a,b // a9,b9 ) )
assume that
A1: not LIN o,a,b and
A2: o,a // o,a9 and
A3: LIN o,b,b9 and
A4: a,b '||' a9,b9 ; ::_thesis: ( o,b // o,b9 & a,b // a9,b9 )
A5: o <> a by A1, DIRAF:31;
consider a2 being Element of OAS such that
A6: Mid a,o,a2 and
A7: o <> a2 by DIRAF:13;
 a,o // o,a2 by A6, DIRAF:def_3;
then consider b2 being Element of OAS such that
A8: b,o // o,b2 and
A9: b,a // a2,b2 by A5, ANALOAF:def_5;
A10: o,b // b2,o by A8, DIRAF:2;
 a,o // o,a2 by A6, DIRAF:def_3;
then  a2,o // o,a by DIRAF:2;
then A11: a2,o // o,a9 by A2, A5, DIRAF:3;
 LIN a,o,a2 by A6, DIRAF:28;
then A12: LIN o,a2,a by DIRAF:30;
A13: o <> b2
proof
assume  o = b2 ; ::_thesis: contradiction
then  o,a2 // a,b by A9, DIRAF:2;
then  o,a2 '||' a,b by DIRAF:def_4;
then  ( LIN o,a2,o & LIN o,a2,b ) by A7, A12, DIRAF:31, DIRAF:33;
hence  contradiction by A1, A7, A12, DIRAF:32; ::_thesis: verum
end;
 Mid b,o,b2 by A8, DIRAF:def_3;
then  LIN b,o,b2 by DIRAF:28;
then A14: LIN b2,o,b by DIRAF:30;
A15: not LIN o,a2,b2
proof
A16: LIN b2,o,o by DIRAF:31;
A17: LIN o,a2,o by DIRAF:31;
assume  LIN o,a2,b2 ; ::_thesis: contradiction
then  LIN b2,o,a by A7, A12, A17, DIRAF:32;
hence  contradiction by A1, A14, A13, A16, DIRAF:32; ::_thesis: verum
end;
 a2,b2 // b,a by A9, DIRAF:2;
then A18: a2,b2 '||' a,b by DIRAF:def_4;
 b <> a by A1, DIRAF:31;
then A19: a2,b2 '||' a9,b9 by A4, A18, DIRAF:23;
A20: a,b // b2,a2 by A9, DIRAF:2;
 Mid b,o,b2 by A8, DIRAF:def_3;
then  LIN b,o,b2 by DIRAF:28;
then A21: LIN o,b,b2 by DIRAF:30;
A22: LIN o,b,o by DIRAF:31;
 o <> b by A1, DIRAF:31;
then A23: LIN o,b2,b9 by A3, A21, A22, DIRAF:32;
then  a2,b2 // b9,a9 by A15, A11, A19, Th7;
then A24: b2,a2 // a9,b9 by DIRAF:2;
 b2,o // o,b9 by A15, A11, A19, A23, Th7;
hence  o,b // o,b9 by A13, A10, DIRAF:3; ::_thesis: a,b // a9,b9
 a2 <> b2 by A15, DIRAF:31;
hence  a,b // a9,b9 by A20, A24, DIRAF:3; ::_thesis: verum
end;

theorem Th9: :: PAPDESAF:9
for OAP being OAffinSpace st OAP is satisfying_DES_1 holds
Lambda OAP is Desarguesian
proof
let OAP be OAffinSpace; ::_thesis: ( OAP is satisfying_DES_1 implies Lambda OAP is Desarguesian )
set AP = Lambda OAP;
assume A1: OAP is satisfying_DES_1 ; ::_thesis: Lambda OAP is Desarguesian
then A2: OAP is satisfying_DES by Th6;
 for A, P, C being Subset of (Lambda OAP)
for o, a, b, c, a9, b9, c9 being Element of (Lambda OAP) st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9
proof
let A, P, C be Subset of (Lambda OAP); ::_thesis: for o, a, b, c, a9, b9, c9 being Element of (Lambda OAP) st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9
let o, a, b, c, a9, b9, c9 be Element of (Lambda OAP); ::_thesis: ( o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )
reconsider o1 = o, a1 = a, b1 = b, c1 = c, a19 = a9, b19 = b9, c19 = c9 as Element of OAP by Th1;
assume that
A3: o in A and
A4: o in P and
A5: o in C and
A6: o <> a and
A7: o <> b and
A8: o <> c and
A9: a in A and
A10: a9 in A and
A11: b in P and
A12: b9 in P and
A13: c in C and
A14: c9 in C and
A15: A is being_line and
A16: P is being_line and
A17: C is being_line and
A18: A <> P and
A19: A <> C and
A20: ( a,b // a9,b9 & a,c // a9,c9 ) ; ::_thesis: b,c // b9,c9
 LIN o,b,b9 by A4, A11, A12, A16, AFF_1:21;
then A21: LIN o1,b1,b19 by Th2;
A22: ( not LIN o1,a1,b1 & not LIN o1,a1,c1 )
proof
A23: now__::_thesis:_not_LIN_o,a,c
assume  LIN o,a,c ; ::_thesis: contradiction
then consider X being Subset of (Lambda OAP) such that
A24: ( X is being_line & o in X ) and
A25: a in X and
A26: c in X by AFF_1:21;
 X = C by A5, A8, A13, A17, A24, A26, AFF_1:18;
hence  contradiction by A3, A6, A9, A15, A19, A24, A25, AFF_1:18; ::_thesis: verum
end;
A27: now__::_thesis:_not_LIN_o,a,b
assume  LIN o,a,b ; ::_thesis: contradiction
then consider X being Subset of (Lambda OAP) such that
A28: ( X is being_line & o in X ) and
A29: a in X and
A30: b in X by AFF_1:21;
 X = P by A4, A7, A11, A16, A28, A30, AFF_1:18;
hence  contradiction by A3, A6, A9, A15, A18, A28, A29, AFF_1:18; ::_thesis: verum
end;
assume  ( LIN o1,a1,b1 or LIN o1,a1,c1 ) ; ::_thesis: contradiction
hence  contradiction by A27, A23, Th2; ::_thesis: verum
end;
 LIN o,c,c9 by A5, A13, A14, A17, AFF_1:21;
then A31: LIN o1,c1,c19 by Th2;
A32: ( a1,b1 '||' a19,b19 & a1,c1 '||' a19,c19 ) by A20, DIRAF:38;
A33: now__::_thesis:_(_a1,o1_//_o1,a19_implies_b,c_//_b9,c9_)
assume A34: a1,o1 // o1,a19 ; ::_thesis: b,c // b9,c9
then A35: ( a1,b1 // b19,a19 & a1,c1 // c19,a19 ) by A21, A31, A22, A32, Th7;
 ( b1,o1 // o1,b19 & c1,o1 // o1,c19 ) by A21, A31, A22, A32, A34, Th7;
then  b1,c1 // c19,b19 by A1, A22, A34, A35, Def7;
then  b1,c1 '||' b19,c19 by DIRAF:def_4;
hence  b,c // b9,c9 by DIRAF:38; ::_thesis: verum
end;
A36: now__::_thesis:_(_o1,a1_//_o1,a19_implies_b,c_//_b9,c9_)
assume A37: o1,a1 // o1,a19 ; ::_thesis: b,c // b9,c9
then A38: ( a1,b1 // a19,b19 & a1,c1 // a19,c19 ) by A21, A31, A22, A32, Th8;
 ( o1,b1 // o1,b19 & o1,c1 // o1,c19 ) by A21, A31, A22, A32, A37, Th8;
then  b1,c1 // b19,c19 by A2, A22, A37, A38, Def6;
then  b1,c1 '||' b19,c19 by DIRAF:def_4;
hence  b,c // b9,c9 by DIRAF:38; ::_thesis: verum
end;
 LIN o,a,a9 by A3, A9, A10, A15, AFF_1:21;
then  LIN o1,a1,a19 by Th2;
then  ( Mid o1,a1,a19 or Mid a1,o1,a19 or Mid o1,a19,a1 ) by DIRAF:29;
hence  b,c // b9,c9 by A33, A36, DIRAF:7, DIRAF:def_3; ::_thesis: verum
end;
hence  Lambda OAP is Desarguesian by AFF_2:def_4; ::_thesis: verum
end;

theorem Th10: :: PAPDESAF:10
for V being RealLinearSpace
for o, u, v, u1, v1 being VECTOR of V
for r being Real st o - u = r * (u1 - o) & r <> 0 & o,v '||' o,v1 & not o,u '||' o,v & u,v '||' u1,v1 holds
( v1 = u1 + (((- r) ") * (v - u)) & v1 = o + (((- r) ") * (v - o)) & v - u = (- r) * (v1 - u1) )
proof
let V be RealLinearSpace; ::_thesis: for o, u, v, u1, v1 being VECTOR of V
for r being Real st o - u = r * (u1 - o) & r <> 0 & o,v '||' o,v1 & not o,u '||' o,v & u,v '||' u1,v1 holds
( v1 = u1 + (((- r) ") * (v - u)) & v1 = o + (((- r) ") * (v - o)) & v - u = (- r) * (v1 - u1) )
let o, u, v, u1, v1 be VECTOR of V; ::_thesis: for r being Real st o - u = r * (u1 - o) & r <> 0 & o,v '||' o,v1 & not o,u '||' o,v & u,v '||' u1,v1 holds
( v1 = u1 + (((- r) ") * (v - u)) & v1 = o + (((- r) ") * (v - o)) & v - u = (- r) * (v1 - u1) )
let r be Real; ::_thesis: ( o - u = r * (u1 - o) & r <> 0 & o,v '||' o,v1 & not o,u '||' o,v & u,v '||' u1,v1 implies ( v1 = u1 + (((- r) ") * (v - u)) & v1 = o + (((- r) ") * (v - o)) & v - u = (- r) * (v1 - u1) ) )
assume that
A1: o - u = r * (u1 - o) and
A2: r <> 0 and
A3: o,v '||' o,v1 and
A4: not o,u '||' o,v and
A5: u,v '||' u1,v1 ; ::_thesis: ( v1 = u1 + (((- r) ") * (v - u)) & v1 = o + (((- r) ") * (v - o)) & v - u = (- r) * (v1 - u1) )
A6: - r <> 0 by A2;
 for r1, r2 being Real st (r1 * (u - o)) + (r2 * (v - o)) = 0. V holds
( r1 = 0 & r2 = 0 )
proof
let r1, r2 be Real; ::_thesis: ( (r1 * (u - o)) + (r2 * (v - o)) = 0. V implies ( r1 = 0 & r2 = 0 ) )
assume  (r1 * (u - o)) + (r2 * (v - o)) = 0. V ; ::_thesis: ( r1 = 0 & r2 = 0 )
then A7: r1 * (u - o) = - (r2 * (v - o)) by RLVECT_1:6
.= r2 * (- (v - o)) by RLVECT_1:25
.= (- r2) * (v - o) by RLVECT_1:24 ;
assume  ( r1 <> 0 or r2 <> 0 ) ; ::_thesis: contradiction
then  ( r1 <> 0 or - r2 <> 0 ) ;
then  ( o,u // o,v or o,u // v,o ) by A7, ANALMETR:14;
hence  contradiction by A4, GEOMTRAP:def_1; ::_thesis: verum
end;
then reconsider X = OASpace V as OAffinSpace by ANALOAF:26;
set w = u1 + (((- r) ") * (v - u));
reconsider p = o, a = u, a1 = u1, b = v, b1 = v1, q = u1 + (((- r) ") * (v - u)) as Element of X by Th3;
 a,b '||' a1,b1 by A5, Th4;
then A8: b,a '||' a1,b1 by DIRAF:22;
 p,b '||' p,b1 by A3, Th4;
then A9: LIN p,b,b1 by DIRAF:def_5;
A10: (- r) * ((u1 + (((- r) ") * (v - u))) - u1) = (- r) * (((- r) ") * (v - u)) by RLSUB_2:61
.= ((- r) * ((- r) ")) * (v - u) by RLVECT_1:def_7
.= 1 * (v - u) by A6, XCMPLX_0:def_7 ;
then A11: v - u = (- r) * ((u1 + (((- r) ") * (v - u))) - u1) by RLVECT_1:def_8;
 ( u,v // u1,u1 + (((- r) ") * (v - u)) or u,v // u1 + (((- r) ") * (v - u)),u1 ) by A10, ANALMETR:14;
then  u,v '||' u1,u1 + (((- r) ") * (v - u)) by GEOMTRAP:def_1;
then  a,b '||' a1,q by Th4;
then A12: b,a '||' a1,q by DIRAF:22;
A13: (- r) * (o - (u1 + (((- r) ") * (v - u)))) = ((- r) * o) - ((- r) * (u1 + (((- r) ") * (v - u)))) by RLVECT_1:34
.= ((- r) * o) - (((- r) * u1) + ((- r) * (((- r) ") * (v - u)))) by RLVECT_1:def_5
.= ((- r) * o) - (((- r) * u1) + (((- r) * ((- r) ")) * (v - u))) by RLVECT_1:def_7
.= ((- r) * o) - (((- r) * u1) + (1 * (v - u))) by A6, XCMPLX_0:def_7
.= ((- r) * o) - (((- r) * u1) + (v - u)) by RLVECT_1:def_8
.= (((- r) * o) - ((- r) * u1)) - (v - u) by RLVECT_1:27
.= ((- r) * (o - u1)) - (v - u) by RLVECT_1:34
.= (r * (- (o - u1))) - (v - u) by RLVECT_1:24
.= (o - u) - (v - u) by A1, RLVECT_1:33
.= o - ((v - u) + u) by RLVECT_1:27
.= o - v by RLSUB_2:61
.= 1 * (o - v) by RLVECT_1:def_8 ;
then  ( v,o // u1 + (((- r) ") * (v - u)),o or v,o // o,u1 + (((- r) ") * (v - u)) ) by ANALMETR:14;
then  ( o,v // u1 + (((- r) ") * (v - u)),o or o,v // o,u1 + (((- r) ") * (v - u)) ) by ANALOAF:12;
then  o,v '||' o,u1 + (((- r) ") * (v - u)) by GEOMTRAP:def_1;
then  p,b '||' p,q by Th4;
then A14: LIN p,b,q by DIRAF:def_5;
1 * (u - o) = (- 1) * (- (u - o)) by RLVECT_1:26
.= (- 1) * (r * (u1 - o)) by A1, RLVECT_1:33
.= ((- 1) * r) * (u1 - o) by RLVECT_1:def_7
.= (- r) * (u1 - o) ;
then  ( o,u // o,u1 or o,u // u1,o ) by ANALMETR:14;
then  o,u '||' o,u1 by GEOMTRAP:def_1;
then  p,a '||' p,a1 by Th4;
then A15: LIN p,a,a1 by DIRAF:def_5;
A16: not LIN p,b,a
proof
assume  LIN p,b,a ; ::_thesis: contradiction
then  p,b '||' p,a by DIRAF:def_5;
then  p,a '||' p,b by DIRAF:22;
hence  contradiction by A4, Th4; ::_thesis: verum
end;
A17: (- r) * ((u1 + (((- r) ") * (v - u))) - o) = r * (- ((u1 + (((- r) ") * (v - u))) - o)) by RLVECT_1:24
.= r * (o - (u1 + (((- r) ") * (v - u)))) by RLVECT_1:33
.= - (- (r * (o - (u1 + (((- r) ") * (v - u)))))) by RLVECT_1:17
.= - (r * (- (o - (u1 + (((- r) ") * (v - u)))))) by RLVECT_1:25
.= - (1 * (o - v)) by A13, RLVECT_1:24
.= - (o - v) by RLVECT_1:def_8
.= v - o by RLVECT_1:33 ;
u1 + (((- r) ") * (v - u)) = o + ((u1 + (((- r) ") * (v - u))) - o) by RLSUB_2:61
.= o + (((- r) ") * (v - o)) by A6, A17, ANALOAF:6 ;
hence  ( v1 = u1 + (((- r) ") * (v - u)) & v1 = o + (((- r) ") * (v - o)) & v - u = (- r) * (v1 - u1) ) by A11, A16, A9, A14, A15, A12, A8, PASCH:4; ::_thesis: verum
end;

Lm1:  for V being RealLinearSpace
for u, v, w being VECTOR of V st u <> v & w <> v & u,v // v,w holds
ex r being Real st
( v - u = r * (w - v) & 0 < r )
proof
let V be RealLinearSpace; ::_thesis: for u, v, w being VECTOR of V st u <> v & w <> v & u,v // v,w holds
ex r being Real st
( v - u = r * (w - v) & 0 < r )
let u, v, w be VECTOR of V; ::_thesis: ( u <> v & w <> v & u,v // v,w implies ex r being Real st
( v - u = r * (w - v) & 0 < r ) )
assume  ( u <> v & w <> v & u,v // v,w ) ; ::_thesis: ex r being Real st
( v - u = r * (w - v) & 0 < r )
then consider a, b being Real such that
A1: a * (v - u) = b * (w - v) and
A2: 0 < a and
A3: 0 < b by ANALOAF:7;
take r = (a ") * b; ::_thesis: ( v - u = r * (w - v) & 0 < r )
 0 < a " by A2, XREAL_1:122;
then A4: 0 * b < r by A3, XREAL_1:68;
v - u = 1 * (v - u) by RLVECT_1:def_8
.= ((a ") * a) * (v - u) by A2, XCMPLX_0:def_7
.= (a ") * (b * (w - v)) by A1, RLVECT_1:def_7
.= r * (w - v) by RLVECT_1:def_7 ;
hence  ( v - u = r * (w - v) & 0 < r ) by A4; ::_thesis: verum
end;

theorem Th11: :: PAPDESAF:11
for V being RealLinearSpace
for OAS being OAffinSpace st OAS = OASpace V holds
OAS is satisfying_DES_1
proof
let V be RealLinearSpace; ::_thesis: for OAS being OAffinSpace st OAS = OASpace V holds
OAS is satisfying_DES_1
let OAS be OAffinSpace; ::_thesis: ( OAS = OASpace V implies OAS is satisfying_DES_1 )
assume A1: OAS = OASpace V ; ::_thesis: OAS is satisfying_DES_1
 for o, a, b, c, a1, b1, c1 being Element of OAS st a,o // o,a1 & b,o // o,b1 & c,o // o,c1 & not LIN o,a,b & not LIN o,a,c & a,b // b1,a1 & a,c // c1,a1 holds
b,c // c1,b1
proof
let o, a, b, c, a1, b1, c1 be Element of OAS; ::_thesis: ( a,o // o,a1 & b,o // o,b1 & c,o // o,c1 & not LIN o,a,b & not LIN o,a,c & a,b // b1,a1 & a,c // c1,a1 implies b,c // c1,b1 )
assume that
A2: a,o // o,a1 and
A3: b,o // o,b1 and
A4: c,o // o,c1 and
A5: not LIN o,a,b and
A6: not LIN o,a,c and
A7: a,b // b1,a1 and
A8: a,c // c1,a1 ; ::_thesis: b,c // c1,b1
reconsider y = o, u = a, v = b, w = c, u1 = a1, v1 = b1, w1 = c1 as VECTOR of V by A1, Th3;
A9: o <> a by A5, DIRAF:31;
A10: now__::_thesis:_(_o_<>_a1_implies_b,c_//_c1,b1_)
A11: ( not y,u '||' y,v & not y,u '||' y,w )
proof
assume  ( y,u '||' y,v or y,u '||' y,w ) ; ::_thesis: contradiction
then  ( y,u // y,v or y,u // v,y or y,u // y,w or y,u // w,y ) by GEOMTRAP:def_1;
then  ( o,a // o,b or o,a // b,o or o,a // o,c or o,a // c,o ) by A1, GEOMTRAP:2;
then  ( o,a '||' o,b or o,a '||' o,c ) by DIRAF:def_4;
hence  contradiction by A5, A6, DIRAF:def_5; ::_thesis: verum
end;
 o,c // c1,o by A4, DIRAF:2;
then  y,w // w1,y by A1, GEOMTRAP:2;
then A12: y,w '||' y,w1 by GEOMTRAP:def_1;
 o,b // b1,o by A3, DIRAF:2;
then  y,v // v1,y by A1, GEOMTRAP:2;
then A13: y,v '||' y,v1 by GEOMTRAP:def_1;
assume A14: o <> a1 ; ::_thesis: b,c // c1,b1
 u,y // y,u1 by A1, A2, GEOMTRAP:2;
then consider r being Real such that
A15: y - u = r * (u1 - y) and
A16: 0 < r by A9, A14, Lm1;
 u,w // w1,u1 by A1, A8, GEOMTRAP:2;
then  u,w '||' u1,w1 by GEOMTRAP:def_1;
then A17: w1 = u1 + (((- r) ") * (w - u)) by A15, A16, A12, A11, Th10;
 u,v // v1,u1 by A1, A7, GEOMTRAP:2;
then  u,v '||' u1,v1 by GEOMTRAP:def_1;
then  v1 = u1 + (((- r) ") * (v - u)) by A15, A16, A13, A11, Th10;
then A18: 1 * (w1 - v1) = (u1 + (((- r) ") * (w - u))) - (u1 + (((- r) ") * (v - u))) by A17, RLVECT_1:def_8
.= (((((- r) ") * (w - u)) + u1) - u1) - (((- r) ") * (v - u)) by RLVECT_1:27
.= (((- r) ") * (w - u)) - (((- r) ") * (v - u)) by RLSUB_2:61
.= ((- r) ") * ((w - u) - (v - u)) by RLVECT_1:34
.= ((- r) ") * (w - ((v - u) + u)) by RLVECT_1:27
.= ((- r) ") * (w - v) by RLSUB_2:61
.= (- (r ")) * (w - v) by XCMPLX_1:222
.= (r ") * (- (w - v)) by RLVECT_1:24
.= (r ") * (v - w) by RLVECT_1:33 ;
 0 < r " by A16, XREAL_1:122;
then  w,v // v1,w1 by A18, ANALOAF:def_1;
then  c,b // b1,c1 by A1, GEOMTRAP:2;
hence  b,c // c1,b1 by DIRAF:2; ::_thesis: verum
end;
now__::_thesis:_(_o_=_a1_implies_b,c_//_c1,b1_)
assume A19: o = a1 ; ::_thesis: b,c // c1,b1
A20: o = c1
proof
 c,o '||' o,c1 by A4, DIRAF:def_4;
then  o,c1 '||' o,c by DIRAF:22;
then A21: LIN o,c1,c by DIRAF:def_5;
A22: LIN o,c1,o by DIRAF:31;
assume A23: o <> c1 ; ::_thesis: contradiction
 a,c '||' c1,o by A8, A19, DIRAF:def_4;
then  o,c1 '||' c,a by DIRAF:22;
then  LIN o,c1,a by A23, A21, DIRAF:33;
hence  contradiction by A6, A23, A21, A22, DIRAF:32; ::_thesis: verum
end;
 o = b1
proof
 b,o '||' o,b1 by A3, DIRAF:def_4;
then  o,b1 '||' o,b by DIRAF:22;
then A24: LIN o,b1,b by DIRAF:def_5;
A25: LIN o,b1,o by DIRAF:31;
assume A26: o <> b1 ; ::_thesis: contradiction
 a,b '||' b1,o by A7, A19, DIRAF:def_4;
then  o,b1 '||' b,a by DIRAF:22;
then  LIN o,b1,a by A26, A24, DIRAF:33;
hence  contradiction by A5, A26, A24, A25, DIRAF:32; ::_thesis: verum
end;
hence  b,c // c1,b1 by A20, DIRAF:4; ::_thesis: verum
end;
hence  b,c // c1,b1 by A10; ::_thesis: verum
end;
hence  OAS is satisfying_DES_1 by Def7; ::_thesis: verum
end;

theorem :: PAPDESAF:12
for V being RealLinearSpace
for OAS being OAffinSpace st OAS = OASpace V holds
( OAS is satisfying_DES_1 & OAS is satisfying_DES ) by Th6, Th11;

Lm2:  for V being RealLinearSpace
for y, u, v being VECTOR of V st y,u '||' y,v & y <> u & y <> v holds
ex r being Real st
( u - y = r * (v - y) & r <> 0 )
proof
let V be RealLinearSpace; ::_thesis: for y, u, v being VECTOR of V st y,u '||' y,v & y <> u & y <> v holds
ex r being Real st
( u - y = r * (v - y) & r <> 0 )
let y, u, v be VECTOR of V; ::_thesis: ( y,u '||' y,v & y <> u & y <> v implies ex r being Real st
( u - y = r * (v - y) & r <> 0 ) )
assume that
A1: y,u '||' y,v and
A2: y <> u and
A3: y <> v ; ::_thesis: ex r being Real st
( u - y = r * (v - y) & r <> 0 )
 ( y,u // y,v or y,u // v,y ) by A1, GEOMTRAP:def_1;
then consider a, b being Real such that
A4: a * (u - y) = b * (v - y) and
A5: ( a <> 0 or b <> 0 ) by ANALMETR:14;
A6: now__::_thesis:_not_b_=_0
assume A7: b = 0 ; ::_thesis: contradiction
then  0. V = a * (u - y) by A4, RLVECT_1:10;
then  u - y = 0. V by A5, A7, RLVECT_1:11;
hence  contradiction by A2, RLVECT_1:21; ::_thesis: verum
end;
A8: now__::_thesis:_not_a_=_0
assume A9: a = 0 ; ::_thesis: contradiction
then  0. V = b * (v - y) by A4, RLVECT_1:10;
then  v - y = 0. V by A5, A9, RLVECT_1:11;
hence  contradiction by A3, RLVECT_1:21; ::_thesis: verum
end;
then A10: a " <> 0 by XCMPLX_1:202;
take r = (a ") * b; ::_thesis: ( u - y = r * (v - y) & r <> 0 )
r * (v - y) = (a ") * (a * (u - y)) by A4, RLVECT_1:def_7
.= ((a ") * a) * (u - y) by RLVECT_1:def_7
.= 1 * (u - y) by A8, XCMPLX_0:def_7
.= u - y by RLVECT_1:def_8 ;
hence  ( u - y = r * (v - y) & r <> 0 ) by A6, A10, XCMPLX_1:6; ::_thesis: verum
end;

Lm3:  for V being RealLinearSpace
for u, v, y being VECTOR of V holds (u - y) - (v - y) = u - v
proof
let V be RealLinearSpace; ::_thesis: for u, v, y being VECTOR of V holds (u - y) - (v - y) = u - v
let u, v, y be VECTOR of V; ::_thesis: (u - y) - (v - y) = u - v
thus (u - y) - (v - y) = u - ((v - y) + y) by RLVECT_1:27
.= u - v by RLSUB_2:61 ; ::_thesis: verum
end;

theorem Th13: :: PAPDESAF:13
for V being RealLinearSpace
for OAS being OAffinSpace st OAS = OASpace V holds
Lambda OAS is Pappian
proof
let V be RealLinearSpace; ::_thesis: for OAS being OAffinSpace st OAS = OASpace V holds
Lambda OAS is Pappian
let OAS be OAffinSpace; ::_thesis: ( OAS = OASpace V implies Lambda OAS is Pappian )
assume A1: OAS = OASpace V ; ::_thesis: Lambda OAS is Pappian
set AS = Lambda OAS;
 for M, N being Subset of (Lambda OAS)
for o, a, b, c, a9, b9, c9 being Element of (Lambda OAS) st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9
proof
let M, N be Subset of (Lambda OAS); ::_thesis: for o, a, b, c, a9, b9, c9 being Element of (Lambda OAS) st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9
let o, a, b, c, a9, b9, c9 be Element of (Lambda OAS); ::_thesis: ( M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 implies a,c9 // c,a9 )
assume that
A2: M is being_line and
A3: N is being_line and
A4: M <> N and
A5: o in M and
A6: o in N and
A7: o <> a and
A8: o <> a9 and
A9: o <> b and
 o <> b9 and
A10: o <> c and
A11: o <> c9 and
A12: a in M and
A13: b in M and
A14: c in M and
A15: a9 in N and
A16: b9 in N and
A17: c9 in N and
A18: a,b9 // b,a9 and
A19: b,c9 // c,b9 ; ::_thesis: a,c9 // c,a9
reconsider o1 = o, a1 = a, b1 = b, c1 = c, a19 = a9, b19 = b9, c19 = c9 as Element of OAS by Th1;
reconsider q = o1, u = a1, v = b1, w = c1, u9 = a19, v9 = b19, w9 = c19 as VECTOR of V by A1, Th3;
 b1,c19 '||' c1,b19 by A19, DIRAF:38;
then A20: v,w9 '||' w,v9 by A1, Th4;
A21: ( not q,v '||' q,w9 & not q,v '||' q,u9 )
proof
assume  ( q,v '||' q,w9 or q,v '||' q,u9 ) ; ::_thesis: contradiction
then  ( o1,b1 '||' o1,c19 or o1,b1 '||' o1,a19 ) by A1, Th4;
then  ( o,b // o,c9 or o,b // o,a9 ) by DIRAF:38;
then  ( LIN o,b,c9 or LIN o,b,a9 ) by AFF_1:def_1;
then  ( c9 in M or a9 in M ) by A2, A5, A9, A13, AFF_1:25;
hence  contradiction by A2, A3, A4, A5, A6, A8, A11, A15, A17, AFF_1:18; ::_thesis: verum
end;
 LIN o,c,b by A2, A5, A13, A14, AFF_1:21;
then  o,c // o,b by AFF_1:def_1;
then  o1,c1 '||' o1,b1 by DIRAF:38;
then  q,w '||' q,v by A1, Th4;
then consider r2 being Real such that
A22: w - q = r2 * (v - q) and
A23: r2 <> 0 by A9, A10, Lm2;
A24: - r2 <> 0 by A23;
 LIN o,a,b by A2, A5, A12, A13, AFF_1:21;
then  o,a // o,b by AFF_1:def_1;
then  o1,a1 '||' o1,b1 by DIRAF:38;
then  q,u '||' q,v by A1, Th4;
then consider r1 being Real such that
A25: u - q = r1 * (v - q) and
A26: r1 <> 0 by A7, A9, Lm2;
A27: (- r1) * (q - v) = r1 * (- (q - v)) by RLVECT_1:24
.= u - q by A25, RLVECT_1:33 ;
 LIN o,c9,b9 by A3, A6, A16, A17, AFF_1:21;
then  o,c9 // o,b9 by AFF_1:def_1;
then  o1,c19 '||' o1,b19 by DIRAF:38;
then A28: q,w9 '||' q,v9 by A1, Th4;
(- r2) * (q - v) = r2 * (- (q - v)) by RLVECT_1:24
.= w - q by A22, RLVECT_1:33 ;
then A29: q - v = ((- r2) ") * (w - q) by A24, ANALOAF:5;
 (- r2) " <> 0 by A24, XCMPLX_1:202;
then v9 = q + (((- ((- r2) ")) ") * (w9 - q)) by A20, A29, A28, A21, Th10
.= q + (((- (- (r2 "))) ") * (w9 - q)) by XCMPLX_1:222
.= q + (r2 * (w9 - q)) ;
then A30: v9 - q = r2 * (w9 - q) by RLSUB_2:61;
 LIN o,a9,b9 by A3, A6, A15, A16, AFF_1:21;
then  o,a9 // o,b9 by AFF_1:def_1;
then  o1,a19 '||' o1,b19 by DIRAF:38;
then A31: q,u9 '||' q,v9 by A1, Th4;
 a1,b19 '||' b1,a19 by A18, DIRAF:38;
then  b1,a19 '||' a1,b19 by DIRAF:22;
then A32: v,u9 '||' u,v9 by A1, Th4;
 r1 " <> 0 by A26, XCMPLX_1:202;
then A33: (r1 ") * r2 <> 0 by A23, XCMPLX_1:6;
set s = r1 * (r2 ");
A34: u - q = r1 * ((r2 ") * (w - q)) by A25, A22, A23, ANALOAF:6
.= (r1 * (r2 ")) * (w - q) by RLVECT_1:def_7 ;
 - r1 <> 0 by A26;
then A35: (- r1) " <> 0 by XCMPLX_1:202;
 - r1 <> 0 by A26;
then  q - v = ((- r1) ") * (u - q) by A27, ANALOAF:6;
then v9 = q + (((- ((- r1) ")) ") * (u9 - q)) by A32, A35, A31, A21, Th10
.= q + (((- (- (r1 "))) ") * (u9 - q)) by XCMPLX_1:222
.= q + (r1 * (u9 - q)) ;
then  v9 - q = r1 * (u9 - q) by RLSUB_2:61;
then u9 - q = (r1 ") * (r2 * (w9 - q)) by A26, A30, ANALOAF:6
.= ((r1 ") * r2) * (w9 - q) by RLVECT_1:def_7 ;
then A36: w9 - q = (((r1 ") * r2) ") * (u9 - q) by A33, ANALOAF:6
.= (((r1 ") ") * (r2 ")) * (u9 - q) by XCMPLX_1:204
.= (r1 * (r2 ")) * (u9 - q) ;
1 * (w9 - u) = w9 - u by RLVECT_1:def_8
.= ((r1 * (r2 ")) * (u9 - q)) - ((r1 * (r2 ")) * (w - q)) by A36, A34, Lm3
.= (r1 * (r2 ")) * ((u9 - q) - (w - q)) by RLVECT_1:34
.= (r1 * (r2 ")) * (u9 - w) by Lm3 ;
then  ( u,w9 // w,u9 or u,w9 // u9,w ) by ANALMETR:14;
then  u,w9 '||' w,u9 by GEOMTRAP:def_1;
then  a1,c19 '||' c1,a19 by A1, Th4;
hence  a,c9 // c,a9 by DIRAF:38; ::_thesis: verum
end;
hence  Lambda OAS is Pappian by AFF_2:def_2; ::_thesis: verum
end;

theorem Th14: :: PAPDESAF:14
for V being RealLinearSpace
for OAS being OAffinSpace st OAS = OASpace V holds
Lambda OAS is Desarguesian by Th9, Th11;

theorem Th15: :: PAPDESAF:15
for AS being AffinSpace st AS is Desarguesian holds
AS is Moufangian
proof
let AS be AffinSpace; ::_thesis: ( AS is Desarguesian implies AS is Moufangian )
assume A1: AS is Desarguesian ; ::_thesis: AS is Moufangian
now__::_thesis:_for_K_being_Subset_of_AS
for_o,_a,_b,_c,_a9,_b9,_c9_being_Element_of_AS_st_K_is_being_line_&_o_in_K_&_c_in_K_&_c9_in_K_&_not_a_in_K_&_o_<>_c_&_a_<>_b_&_LIN_o,a,a9_&_LIN_o,b,b9_&_a,b_//_a9,b9_&_a,c_//_a9,c9_&_a,b_//_K_holds_
b,c_//_b9,c9
let K be Subset of AS; ::_thesis: for o, a, b, c, a9, b9, c9 being Element of AS st K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & a,b // K holds
b,c // b9,c9
let o, a, b, c, a9, b9, c9 be Element of AS; ::_thesis: ( K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & a,b // K implies b,c // b9,c9 )
assume that
A2: K is being_line and
A3: o in K and
A4: ( c in K & c9 in K ) and
A5: not a in K and
A6: o <> c and
A7: a <> b and
A8: LIN o,a,a9 and
A9: LIN o,b,b9 and
A10: ( a,b // a9,b9 & a,c // a9,c9 ) and
A11: a,b // K ; ::_thesis: b,c // b9,c9
set A = Line (o,a);
set P = Line (o,b);
A12: o in Line (o,a) by A3, A5, AFF_1:24;
A13: now__::_thesis:_not_o_=_b
assume A14: o = b ; ::_thesis: contradiction
 b,a // K by A11, AFF_1:34;
hence  contradiction by A2, A3, A5, A14, AFF_1:23; ::_thesis: verum
end;
then A15: b in Line (o,b) by AFF_1:24;
A16: a in Line (o,a) by A3, A5, AFF_1:24;
A17: Line (o,a) is being_line by A3, A5, AFF_1:24;
A18: Line (o,a) <> Line (o,b)
proof
assume  Line (o,a) = Line (o,b) ; ::_thesis: contradiction
then  a,b // Line (o,a) by A17, A16, A15, AFF_1:40, AFF_1:41;
hence  contradiction by A3, A5, A7, A11, A12, A16, AFF_1:45, AFF_1:53; ::_thesis: verum
end;
A19: ( Line (o,b) is being_line & o in Line (o,b) ) by A13, AFF_1:24;
then A20: b9 in Line (o,b) by A9, A13, A15, AFF_1:25;
 a9 in Line (o,a) by A3, A5, A8, A17, A12, A16, AFF_1:25;
hence  b,c // b9,c9 by A1, A2, A3, A4, A5, A6, A10, A13, A17, A12, A16, A19, A15, A20, A18, AFF_2:def_4; ::_thesis: verum
end;
hence  AS is Moufangian by AFF_2:def_7; ::_thesis: verum
end;

theorem Th16: :: PAPDESAF:16
for V being RealLinearSpace
for OAS being OAffinSpace st OAS = OASpace V holds
Lambda OAS is Moufangian
proof
let V be RealLinearSpace; ::_thesis: for OAS being OAffinSpace st OAS = OASpace V holds
Lambda OAS is Moufangian
let OAS be OAffinSpace; ::_thesis: ( OAS = OASpace V implies Lambda OAS is Moufangian )
assume  OAS = OASpace V ; ::_thesis: Lambda OAS is Moufangian
then  Lambda OAS is Desarguesian by Th9, Th11;
hence  Lambda OAS is Moufangian by Th15; ::_thesis: verum
end;

theorem Th17: :: PAPDESAF:17
for V being RealLinearSpace
for OAS being OAffinSpace st OAS = OASpace V holds
Lambda OAS is translational
proof
let V be RealLinearSpace; ::_thesis: for OAS being OAffinSpace st OAS = OASpace V holds
Lambda OAS is translational
let OAS be OAffinSpace; ::_thesis: ( OAS = OASpace V implies Lambda OAS is translational )
assume A1: OAS = OASpace V ; ::_thesis: Lambda OAS is translational
set AS = Lambda OAS;
 for A, P, C being Subset of (Lambda OAS)
for a, b, c, a9, b9, c9 being Element of (Lambda OAS) st A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9
proof
let A, P, C be Subset of (Lambda OAS); ::_thesis: for a, b, c, a9, b9, c9 being Element of (Lambda OAS) st A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9
let a, b, c, a9, b9, c9 be Element of (Lambda OAS); ::_thesis: ( A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )
assume that
A2: A // P and
A3: A // C and
A4: a in A and
A5: a9 in A and
A6: b in P and
A7: b9 in P and
A8: c in C and
A9: c9 in C and
A10: A is being_line and
A11: P is being_line and
A12: C is being_line and
A13: A <> P and
A14: A <> C and
A15: a,b // a9,b9 and
A16: a,c // a9,c9 ; ::_thesis: b,c // b9,c9
reconsider a1 = a, b1 = b, c1 = c, a19 = a9, b19 = b9, c19 = c9 as Element of OAS by Th1;
reconsider u = a1, v = b1, w = c1, u9 = a19 as VECTOR of V by A1, Th3;
A17: now__::_thesis:_(_a_<>_a9_implies_b,c_//_b9,c9_)
assume A18: a <> a9 ; ::_thesis: b,c // b9,c9
A19: not LIN a1,a19,b1
proof
assume  LIN a1,a19,b1 ; ::_thesis: contradiction
then  LIN a,a9,b by Th2;
then  b in A by A4, A5, A10, A18, AFF_1:25;
hence  contradiction by A2, A6, A13, AFF_1:45; ::_thesis: verum
end;
A20: not LIN a1,a19,c1
proof
assume  LIN a1,a19,c1 ; ::_thesis: contradiction
then  LIN a,a9,c by Th2;
then  c in A by A4, A5, A10, A18, AFF_1:25;
hence  contradiction by A3, A8, A14, AFF_1:45; ::_thesis: verum
end;
 a,a9 // c,c9 by A3, A4, A5, A8, A9, AFF_1:39;
then A21: a1,a19 '||' c1,c19 by DIRAF:38;
 a,a9 // b,b9 by A2, A4, A5, A6, A7, AFF_1:39;
then A22: a1,a19 '||' b1,b19 by DIRAF:38;
set v99 = (u9 + v) - u;
set w99 = (u9 + w) - u;
reconsider b199 = (u9 + v) - u, c199 = (u9 + w) - u as Element of OAS by A1, Th3;
((u9 + w) - u) - ((u9 + v) - u) = (u9 + w) - (((u9 + v) - u) + u) by RLVECT_1:27
.= (u9 + w) - (u9 + v) by RLSUB_2:61
.= ((w + u9) - u9) - v by RLVECT_1:27
.= w - v by RLSUB_2:61 ;
then  v,w // (u9 + v) - u,(u9 + w) - u by ANALOAF:15;
then A23: v,w '||' (u9 + v) - u,(u9 + w) - u by GEOMTRAP:def_1;
 u,u9 // v,(u9 + v) - u by ANALOAF:16;
then  u,u9 '||' v,(u9 + v) - u by GEOMTRAP:def_1;
then A24: a1,a19 '||' b1,b199 by A1, Th4;
 u,w // u9,(u9 + w) - u by ANALOAF:16;
then  u,w '||' u9,(u9 + w) - u by GEOMTRAP:def_1;
then A25: a1,c1 '||' a19,c199 by A1, Th4;
 u,u9 // w,(u9 + w) - u by ANALOAF:16;
then  u,u9 '||' w,(u9 + w) - u by GEOMTRAP:def_1;
then A26: a1,a19 '||' c1,c199 by A1, Th4;
 u,v // u9,(u9 + v) - u by ANALOAF:16;
then  u,v '||' u9,(u9 + v) - u by GEOMTRAP:def_1;
then A27: a1,b1 '||' a19,b199 by A1, Th4;
 a1,c1 '||' a19,c19 by A16, DIRAF:38;
then A28: c199 = c19 by A20, A21, A26, A25, PASCH:5;
 a1,b1 '||' a19,b19 by A15, DIRAF:38;
then  b199 = b19 by A19, A22, A24, A27, PASCH:5;
then  b1,c1 '||' b19,c19 by A1, A28, A23, Th4;
hence  b,c // b9,c9 by DIRAF:38; ::_thesis: verum
end;
now__::_thesis:_(_a_=_a9_implies_b,c_//_b9,c9_)
assume A29: a = a9 ; ::_thesis: b,c // b9,c9
A30: c = c9
proof
 LIN a,c,c9 by A16, A29, AFF_1:def_1;
then A31: LIN c,c9,a by AFF_1:6;
assume  c <> c9 ; ::_thesis: contradiction
then  a in C by A8, A9, A12, A31, AFF_1:25;
hence  contradiction by A3, A4, A14, AFF_1:45; ::_thesis: verum
end;
 b = b9
proof
 LIN a,b,b9 by A15, A29, AFF_1:def_1;
then A32: LIN b,b9,a by AFF_1:6;
assume  b <> b9 ; ::_thesis: contradiction
then  a in P by A6, A7, A11, A32, AFF_1:25;
hence  contradiction by A2, A4, A13, AFF_1:45; ::_thesis: verum
end;
hence  b,c // b9,c9 by A30, AFF_1:2; ::_thesis: verum
end;
hence  b,c // b9,c9 by A17; ::_thesis: verum
end;
hence  Lambda OAS is translational by AFF_2:def_11; ::_thesis: verum
end;

theorem Th18: :: PAPDESAF:18
for OAS being OAffinSpace holds Lambda OAS is Fanoian
proof
let OAS be OAffinSpace; ::_thesis: Lambda OAS is Fanoian
set AS = Lambda OAS;
 for a, b, c, d being Element of (Lambda OAS) st a,b // c,d & a,c // b,d & a,d // b,c holds
a,b // a,c
proof
let a, b, c, d be Element of (Lambda OAS); ::_thesis: ( a,b // c,d & a,c // b,d & a,d // b,c implies a,b // a,c )
assume that
A1: a,b // c,d and
A2: a,c // b,d and
A3: a,d // b,c ; ::_thesis: a,b // a,c
reconsider a1 = a, b1 = b, c1 = c, d1 = d as Element of OAS by Th1;
set P = Line (a,d);
set Q = Line (b,c);
assume A4: not a,b // a,c ; ::_thesis: contradiction
then A5: a <> d by A1, AFF_1:4;
then A6: Line (a,d) is being_line by AFF_1:def_3;
A7: not LIN a1,b1,c1
proof
assume  LIN a1,b1,c1 ; ::_thesis: contradiction
then  a1,b1 '||' a1,c1 by DIRAF:def_5;
hence  contradiction by A4, DIRAF:38; ::_thesis: verum
end;
 ( a1,b1 '||' c1,d1 & a1,c1 '||' b1,d1 ) by A1, A2, DIRAF:38;
then consider x1 being Element of OAS such that
A8: LIN x1,a1,d1 and
A9: LIN x1,b1,c1 by A7, PASCH:25;
reconsider x = x1 as Element of (Lambda OAS) by Th1;
A10: d in Line (a,d) by AFF_1:15;
 x1,a1 '||' x1,d1 by A8, DIRAF:def_5;
then  x,a // x,d by DIRAF:38;
then  LIN x,a,d by AFF_1:def_1;
then  LIN a,d,x by AFF_1:6;
then A11: x in Line (a,d) by AFF_1:def_2;
A12: ( a in Line (a,d) & b in Line (b,c) ) by AFF_1:15;
 x1,b1 '||' x1,c1 by A9, DIRAF:def_5;
then  x,b // x,c by DIRAF:38;
then  LIN x,b,c by AFF_1:def_1;
then  LIN b,c,x by AFF_1:6;
then A13: x in Line (b,c) by AFF_1:def_2;
A14: c in Line (b,c) by AFF_1:15;
A15: not LIN a,b,c by A4, AFF_1:def_1;
then A16: b <> c by AFF_1:7;
then  Line (b,c) is being_line by AFF_1:def_3;
then  Line (a,d) // Line (b,c) by A3, A16, A5, A6, A10, A12, A14, AFF_1:38;
then  Line (a,d) = Line (b,c) by A11, A13, AFF_1:45;
hence  contradiction by A15, A6, A12, A14, AFF_1:21; ::_thesis: verum
end;
hence  Lambda OAS is Fanoian by Def1; ::_thesis: verum
end;

registration
clusterV52() non trivial OAffinSpace-like Pappian Desarguesian Moufangian translation for AffinStruct ;
existence
 ex b1 being OAffinSpace st
( b1 is Pappian & b1 is Desarguesian & b1 is Moufangian & b1 is translation )
proof
consider V being RealLinearSpace such that
A1: ex u, v being VECTOR of V st
for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) by FUNCSDOM:23;
reconsider X = OASpace V as OAffinSpace by A1, ANALOAF:26;
take  X ; ::_thesis: ( X is Pappian & X is Desarguesian & X is Moufangian & X is translation )
set AS = Lambda X;
A2: ( Lambda X is Moufangian & Lambda X is translational ) by Th16, Th17;
 ( Lambda X is Pappian & Lambda X is Desarguesian ) by Th9, Th11, Th13;
hence  ( X is Pappian & X is Desarguesian & X is Moufangian & X is translation ) by A2, Def2, Def3, Def4, Def5; ::_thesis: verum
end;
end;

registration
clusterV52() non trivial strict AffinSpace-like 2-dimensional Pappian Desarguesian Moufangian translational Fanoian for AffinStruct ;
existence
 ex b1 being AffinPlane st
( b1 is strict & b1 is Fanoian & b1 is Pappian & b1 is Desarguesian & b1 is Moufangian & b1 is translational )
proof
consider V being RealLinearSpace such that
A1: ex u, v being VECTOR of V st
( ( for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w being VECTOR of V ex a, b being Real st w = (a * u) + (b * v) ) ) by FUNCSDOM:23;
reconsider OAS = OASpace V as OAffinPlane by A1, ANALOAF:28;
take X = Lambda OAS; ::_thesis: ( X is strict & X is Fanoian & X is Pappian & X is Desarguesian & X is Moufangian & X is translational )
A2: X is Pappian by Th13;
then  X is Moufangian by AFF_2:11, AFF_2:12;
hence  ( X is strict & X is Fanoian & X is Pappian & X is Desarguesian & X is Moufangian & X is translational ) by A2, Th18, AFF_2:11, AFF_2:14; ::_thesis: verum
end;
end;

registration
clusterV52() non trivial strict AffinSpace-like Pappian Desarguesian Moufangian translational Fanoian for AffinStruct ;
existence
 ex b1 being AffinSpace st
( b1 is strict & b1 is Fanoian & b1 is Pappian & b1 is Desarguesian & b1 is Moufangian & b1 is translational )
proof
consider V being RealLinearSpace such that
A1: ex u, v being VECTOR of V st
for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) by FUNCSDOM:23;
reconsider X = OASpace V as OAffinSpace by A1, ANALOAF:26;
take  Lambda X ; ::_thesis: ( Lambda X is strict & Lambda X is Fanoian & Lambda X is Pappian & Lambda X is Desarguesian & Lambda X is Moufangian & Lambda X is translational )
thus  ( Lambda X is strict & Lambda X is Fanoian & Lambda X is Pappian & Lambda X is Desarguesian & Lambda X is Moufangian & Lambda X is translational ) by Th13, Th14, Th16, Th17, Th18; ::_thesis: verum
end;
end;

registration
let OAS be OAffinSpace;
cluster Lambda OAS ->  Fanoian ;
correctness
coherence
Lambda OAS is Fanoian ;
by Th18;
end;

registration
let OAS be Pappian OAffinSpace;
cluster Lambda OAS ->  Pappian ;
correctness
coherence
Lambda OAS is Pappian ;
by Def2;
end;

registration
let OAS be Desarguesian OAffinSpace;
cluster Lambda OAS ->  Desarguesian ;
correctness
coherence
Lambda OAS is Desarguesian ;
by Def3;
end;

registration
let OAS be Moufangian OAffinSpace;
cluster Lambda OAS ->  Moufangian ;
correctness
coherence
Lambda OAS is Moufangian ;
by Def4;
end;

registration
let OAS be translation OAffinSpace;
cluster Lambda OAS ->  translational ;
correctness
coherence
Lambda OAS is translational ;
by Def5;
end;