:: EUCLMETR semantic presentation

begin

definition
let IT be OrtAfSp;
attrIT is Euclidean  means :Def1: :: EUCLMETR:def 1
 for a, b, c, d being Element of IT st a,b _|_ c,d & b,c _|_ a,d holds
b,d _|_ a,c;
end;

:: deftheorem Def1 defines Euclidean EUCLMETR:def_1_:_
 for IT being OrtAfSp holds
( IT is Euclidean iff for a, b, c, d being Element of IT st a,b _|_ c,d & b,c _|_ a,d holds
b,d _|_ a,c );

definition
let IT be OrtAfSp;
attrIT is Pappian  means :Def2: :: EUCLMETR:def 2
 Af IT is Pappian ;
end;

:: deftheorem Def2 defines Pappian EUCLMETR:def_2_:_
 for IT being OrtAfSp holds
( IT is Pappian iff Af IT is Pappian );

definition
let IT be OrtAfSp;
attrIT is Desarguesian  means :Def3: :: EUCLMETR:def 3
 Af IT is Desarguesian ;
end;

:: deftheorem Def3 defines Desarguesian EUCLMETR:def_3_:_
 for IT being OrtAfSp holds
( IT is Desarguesian iff Af IT is Desarguesian );

definition
let IT be OrtAfSp;
attrIT is Fanoian  means :Def4: :: EUCLMETR:def 4
 Af IT is Fanoian ;
end;

:: deftheorem Def4 defines Fanoian EUCLMETR:def_4_:_
 for IT being OrtAfSp holds
( IT is Fanoian iff Af IT is Fanoian );

definition
let IT be OrtAfSp;
attrIT is Moufangian  means :Def5: :: EUCLMETR:def 5
 Af IT is Moufangian ;
end;

:: deftheorem Def5 defines Moufangian EUCLMETR:def_5_:_
 for IT being OrtAfSp holds
( IT is Moufangian iff Af IT is Moufangian );

definition
let IT be OrtAfSp;
attrIT is translation  means :Def6: :: EUCLMETR:def 6
 Af IT is translational ;
end;

:: deftheorem Def6 defines translation EUCLMETR:def_6_:_
 for IT being OrtAfSp holds
( IT is translation iff Af IT is translational );

definition
let IT be OrtAfSp;
attrIT is Homogeneous  means :Def7: :: EUCLMETR:def 7
 for o, a, a1, b, b1, c, c1 being Element of IT st o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b holds
b,c _|_ b1,c1;
end;

:: deftheorem Def7 defines Homogeneous EUCLMETR:def_7_:_
 for IT being OrtAfSp holds
( IT is Homogeneous iff for o, a, a1, b, b1, c, c1 being Element of IT st o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b holds
b,c _|_ b1,c1 );


theorem Th1: :: EUCLMETR:1
for MP being OrtAfSp
for a, b, c being Element of MP st not LIN a,b,c holds
( a <> b & b <> c & a <> c )
proof
let MP be OrtAfSp; ::_thesis: for a, b, c being Element of MP st not LIN a,b,c holds
( a <> b & b <> c & a <> c )
let a, b, c be Element of MP; ::_thesis: ( not LIN a,b,c implies ( a <> b & b <> c & a <> c ) )
assume A1: not LIN a,b,c ; ::_thesis: ( a <> b & b <> c & a <> c )
reconsider b9 = b, a9 = a, c9 = c as Element of (Af MP) by ANALMETR:35;
assume  ( not a <> b or not b <> c or not a <> c ) ; ::_thesis: contradiction
then  LIN a9,b9,c9 by AFF_1:7;
hence  contradiction by A1, ANALMETR:40; ::_thesis: verum
end;

theorem Th2: :: EUCLMETR:2
for MS being OrtAfPl
for a, b, c, d being Element of MS
for K being Subset of the carrier of MS st a,b _|_ K & c,d _|_ K holds
( a,b // c,d & a,b // d,c )
proof
let MS be OrtAfPl; ::_thesis: for a, b, c, d being Element of MS
for K being Subset of the carrier of MS st a,b _|_ K & c,d _|_ K holds
( a,b // c,d & a,b // d,c )
let a, b, c, d be Element of MS; ::_thesis: for K being Subset of the carrier of MS st a,b _|_ K & c,d _|_ K holds
( a,b // c,d & a,b // d,c )
let K be Subset of MS; ::_thesis: ( a,b _|_ K & c,d _|_ K implies ( a,b // c,d & a,b // d,c ) )
assume that
A1: a,b _|_ K and
A2: c,d _|_ K ; ::_thesis: ( a,b // c,d & a,b // d,c )
reconsider K9 = K as Subset of (Af MS) by ANALMETR:42;
 K is being_line by A1, ANALMETR:44;
then  K9 is being_line by ANALMETR:43;
then consider p9, q9 being Element of (Af MS) such that
A3: ( p9 in K9 & q9 in K9 ) and
A4: p9 <> q9 by AFF_1:19;
reconsider p = p9, q = q9 as Element of MS by ANALMETR:35;
 ( a,b _|_ p,q & c,d _|_ p,q ) by A1, A2, A3, ANALMETR:53;
hence  a,b // c,d by A4, ANALMETR:63; ::_thesis: a,b // d,c
hence  a,b // d,c by ANALMETR:59; ::_thesis: verum
end;

theorem :: EUCLMETR:3
for MS being OrtAfPl
for a, b being Element of MS
for A, K being Subset of the carrier of MS st a <> b & ( a,b _|_ K or b,a _|_ K ) & a,b _|_ A holds
K // A
proof
let MS be OrtAfPl; ::_thesis: for a, b being Element of MS
for A, K being Subset of the carrier of MS st a <> b & ( a,b _|_ K or b,a _|_ K ) & a,b _|_ A holds
K // A
let a, b be Element of MS; ::_thesis: for A, K being Subset of the carrier of MS st a <> b & ( a,b _|_ K or b,a _|_ K ) & a,b _|_ A holds
K // A
let A, K be Subset of MS; ::_thesis: ( a <> b & ( a,b _|_ K or b,a _|_ K ) & a,b _|_ A implies K // A )
assume that
A1: a <> b and
A2: ( a,b _|_ K or b,a _|_ K ) and
A3: a,b _|_ A ; ::_thesis: K // A
 a,b _|_ K by A2, ANALMETR:49;
then consider p, q being Element of MS such that
A4: ( p <> q & K = Line (p,q) ) and
A5: a,b _|_ p,q by ANALMETR:def_13;
consider r, s being Element of MS such that
A6: ( r <> s & A = Line (r,s) ) and
A7: a,b _|_ r,s by A3, ANALMETR:def_13;
 p,q // r,s by A1, A5, A7, ANALMETR:63;
hence  K // A by A4, A6, ANALMETR:def_15; ::_thesis: verum
end;

theorem Th4: :: EUCLMETR:4
for MP being OrtAfSp
for x, y, z being Element of MP st LIN x,y,z holds
( LIN x,z,y & LIN y,x,z & LIN y,z,x & LIN z,x,y & LIN z,y,x )
proof
let MP be OrtAfSp; ::_thesis: for x, y, z being Element of MP st LIN x,y,z holds
( LIN x,z,y & LIN y,x,z & LIN y,z,x & LIN z,x,y & LIN z,y,x )
let x, y, z be Element of MP; ::_thesis: ( LIN x,y,z implies ( LIN x,z,y & LIN y,x,z & LIN y,z,x & LIN z,x,y & LIN z,y,x ) )
assume A1: LIN x,y,z ; ::_thesis: ( LIN x,z,y & LIN y,x,z & LIN y,z,x & LIN z,x,y & LIN z,y,x )
reconsider x9 = x, y9 = y, z9 = z as Element of (Af MP) by ANALMETR:35;
A2: LIN x9,y9,z9 by A1, ANALMETR:40;
then A3: ( LIN y9,z9,x9 & LIN z9,x9,y9 ) by AFF_1:6;
A4: LIN z9,y9,x9 by A2, AFF_1:6;
 ( LIN x9,z9,y9 & LIN y9,x9,z9 ) by A2, AFF_1:6;
hence  ( LIN x,z,y & LIN y,x,z & LIN y,z,x & LIN z,x,y & LIN z,y,x ) by A3, A4, ANALMETR:40; ::_thesis: verum
end;

theorem Th5: :: EUCLMETR:5
for MS being OrtAfPl
for a, b, c being Element of MS st not LIN a,b,c holds
ex d being Element of MS st
( d,a _|_ b,c & d,b _|_ a,c )
proof
let MS be OrtAfPl; ::_thesis: for a, b, c being Element of MS st not LIN a,b,c holds
ex d being Element of MS st
( d,a _|_ b,c & d,b _|_ a,c )
let a, b, c be Element of MS; ::_thesis: ( not LIN a,b,c implies ex d being Element of MS st
( d,a _|_ b,c & d,b _|_ a,c ) )
set A = Line (a,c);
set K = Line (b,c);
reconsider A9 = Line (a,c), K9 = Line (b,c) as Subset of (Af MS) by ANALMETR:42;
reconsider a9 = a, b9 = b, c9 = c as Element of (Af MS) by ANALMETR:35;
 K9 = Line (b9,c9) by ANALMETR:41;
then A1: ( b9 in K9 & c9 in K9 ) by AFF_1:15;
assume A2: not LIN a,b,c ; ::_thesis: ex d being Element of MS st
( d,a _|_ b,c & d,b _|_ a,c )
then  a <> c by Th1;
then  Line (a,c) is being_line by ANALMETR:def_12;
then consider P being Subset of MS such that
A3: b in P and
A4: Line (a,c) _|_ P by CONMETR:3;
 b <> c by A2, Th1;
then  Line (b,c) is being_line by ANALMETR:def_12;
then consider Q being Subset of MS such that
A5: a in Q and
A6: Line (b,c) _|_ Q by CONMETR:3;
reconsider P9 = P, Q9 = Q as Subset of (Af MS) by ANALMETR:42;
 Q is being_line by A6, ANALMETR:44;
then A7: Q9 is being_line by ANALMETR:43;
A8: A9 = Line (a9,c9) by ANALMETR:41;
then A9: c9 in A9 by AFF_1:15;
A10: not P9 // Q9
proof
assume  P9 // Q9 ; ::_thesis: contradiction
then  P // Q by ANALMETR:46;
then  Line (a,c) _|_ Q by A4, ANALMETR:52;
then  Line (a,c) // Line (b,c) by A6, ANALMETR:65;
then  A9 // K9 by ANALMETR:46;
then  b9 in A9 by A9, A1, AFF_1:45;
then  LIN a9,c9,b9 by A8, AFF_1:def_2;
then  LIN a9,b9,c9 by AFF_1:6;
hence  contradiction by A2, ANALMETR:40; ::_thesis: verum
end;
 P is being_line by A4, ANALMETR:44;
then  P9 is being_line by ANALMETR:43;
then consider d9 being Element of (Af MS) such that
A11: ( d9 in P9 & d9 in Q9 ) by A7, A10, AFF_1:58;
reconsider d = d9 as Element of MS by ANALMETR:35;
take  d ; ::_thesis: ( d,a _|_ b,c & d,b _|_ a,c )
 a9 in A9 by A8, AFF_1:15;
hence  ( d,a _|_ b,c & d,b _|_ a,c ) by A3, A4, A5, A6, A9, A1, A11, ANALMETR:56; ::_thesis: verum
end;

theorem Th6: :: EUCLMETR:6
for MS being OrtAfPl
for a, b, c, d1, d2 being Element of MS st not LIN a,b,c & d1,a _|_ b,c & d1,b _|_ a,c & d2,a _|_ b,c & d2,b _|_ a,c holds
d1 = d2
proof
let MS be OrtAfPl; ::_thesis: for a, b, c, d1, d2 being Element of MS st not LIN a,b,c & d1,a _|_ b,c & d1,b _|_ a,c & d2,a _|_ b,c & d2,b _|_ a,c holds
d1 = d2
let a, b, c, d1, d2 be Element of MS; ::_thesis: ( not LIN a,b,c & d1,a _|_ b,c & d1,b _|_ a,c & d2,a _|_ b,c & d2,b _|_ a,c implies d1 = d2 )
assume that
A1: not LIN a,b,c and
A2: d1,a _|_ b,c and
A3: d1,b _|_ a,c and
A4: d2,a _|_ b,c and
A5: d2,b _|_ a,c ; ::_thesis: d1 = d2
reconsider a9 = a, b9 = b, c9 = c, d19 = d1, d29 = d2 as Element of (Af MS) by ANALMETR:35;
assume A6: d1 <> d2 ; ::_thesis: contradiction
 b <> c by A1, Th1;
then  d1,a // d2,a by A2, A4, ANALMETR:63;
then  d19,a9 // d29,a9 by ANALMETR:36;
then  a9,d19 // a9,d29 by AFF_1:4;
then  LIN a9,d19,d29 by AFF_1:def_1;
then A7: LIN d19,d29,a9 by AFF_1:6;
 a <> c by A1, Th1;
then  d1,b // d2,b by A3, A5, ANALMETR:63;
then  d19,b9 // d29,b9 by ANALMETR:36;
then  b9,d19 // b9,d29 by AFF_1:4;
then  LIN b9,d19,d29 by AFF_1:def_1;
then A8: LIN d19,d29,b9 by AFF_1:6;
set X9 = Line (a9,b9);
reconsider X = Line (a9,b9) as Subset of MS by ANALMETR:42;
A9: b <> a by A1, Th1;
then A10: Line (a9,b9) is being_line by AFF_1:def_3;
then A11: X is being_line by ANALMETR:43;
A12: a9 in Line (a9,b9) by AFF_1:15;
A13: b9 in Line (a9,b9) by AFF_1:15;
 LIN d19,d29,d29 by AFF_1:7;
then A14: d2 in X by A6, A9, A7, A8, A10, A12, A13, AFF_1:8, AFF_1:25;
 LIN d19,d29,d19 by AFF_1:7;
then A15: d1 in X by A6, A9, A7, A8, A10, A12, A13, AFF_1:8, AFF_1:25;
 ( a <> d1 or a <> d2 ) by A6;
then A16: b,c _|_ X by A2, A4, A12, A15, A14, A11, ANALMETR:55;
 ( b <> d1 or b <> d2 ) by A6;
then  a,c _|_ X by A3, A5, A13, A15, A14, A11, ANALMETR:55;
then  a,c // b,c by A16, Th2;
then  a9,c9 // b9,c9 by ANALMETR:36;
then  c9,b9 // c9,a9 by AFF_1:4;
then  LIN c9,b9,a9 by AFF_1:def_1;
then  LIN a9,b9,c9 by AFF_1:6;
hence  contradiction by A1, ANALMETR:40; ::_thesis: verum
end;

theorem Th7: :: EUCLMETR:7
for MS being OrtAfPl
for a, b, c, d being Element of MS st a,b _|_ c,d & b,c _|_ a,d & LIN a,b,c & not a = c & not a = b holds
b = c
proof
let MS be OrtAfPl; ::_thesis: for a, b, c, d being Element of MS st a,b _|_ c,d & b,c _|_ a,d & LIN a,b,c & not a = c & not a = b holds
b = c
let a, b, c, d be Element of MS; ::_thesis: ( a,b _|_ c,d & b,c _|_ a,d & LIN a,b,c & not a = c & not a = b implies b = c )
assume that
A1: a,b _|_ c,d and
A2: b,c _|_ a,d and
A3: LIN a,b,c ; ::_thesis: ( a = c or a = b or b = c )
assume A4: ( not a = c & not a = b & not b = c ) ; ::_thesis: contradiction
 LIN c,b,a by A3, Th4;
then  c,b // c,a by ANALMETR:def_10;
then  a,c // b,c by ANALMETR:59;
then A5: a,c _|_ a,d by A2, A4, ANALMETR:62;
reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of (Af MS) by ANALMETR:35;
 LIN a9,b9,c9 by A3, ANALMETR:40;
then consider A9 being Subset of (Af MS) such that
A6: A9 is being_line and
A7: a9 in A9 and
A8: b9 in A9 and
A9: c9 in A9 by AFF_1:21;
reconsider A = A9 as Subset of MS by ANALMETR:42;
A10: A is being_line by A6, ANALMETR:43;
then A11: c,d _|_ A by A1, A4, A7, A8, ANALMETR:55;
 a,b // a,c by A3, ANALMETR:def_10;
then  a,c _|_ c,d by A1, A4, ANALMETR:62;
then  c,d // a,d by A4, A5, ANALMETR:63;
then  d,c // d,a by ANALMETR:59;
then  LIN d,c,a by ANALMETR:def_10;
then  LIN a,c,d by Th4;
then  LIN a9,c9,d9 by ANALMETR:40;
then  d in A by A4, A6, A7, A9, AFF_1:25;
then A12: c = d by A9, A11, ANALMETR:51;
 a,d _|_ A by A2, A4, A8, A9, A10, ANALMETR:55;
hence  contradiction by A4, A7, A9, A12, ANALMETR:51; ::_thesis: verum
end;

theorem Th8: :: EUCLMETR:8
for MS being OrtAfPl holds
( MS is Euclidean iff MS is satisfying_3H )
proof
let MS be OrtAfPl; ::_thesis: ( MS is Euclidean iff MS is satisfying_3H )
A1: now__::_thesis:_(_MS_is_satisfying_3H_implies_MS_is_Euclidean_)
assume A2: MS is satisfying_3H ; ::_thesis: MS is Euclidean
now__::_thesis:_for_a,_b,_c,_d_being_Element_of_MS_st_a,b__|__c,d_&_b,c__|__a,d_holds_
b,d__|__a,c
let a, b, c, d be Element of MS; ::_thesis: ( a,b _|_ c,d & b,c _|_ a,d implies b,d _|_ a,c )
assume that
A3: a,b _|_ c,d and
A4: b,c _|_ a,d ; ::_thesis: b,d _|_ a,c
A5: now__::_thesis:_(_not_LIN_a,b,c_implies_b,d__|__a,c_)
A6: ( d,a _|_ c,b & d,c _|_ a,b ) by A3, A4, ANALMETR:61;
assume A7: not LIN a,b,c ; ::_thesis: b,d _|_ a,c
then consider d1 being Element of MS such that
A8: d1,a _|_ b,c and
A9: ( d1,b _|_ a,c & d1,c _|_ a,b ) by A2, CONAFFM:def_3;
A10: not LIN a,c,b by A7, Th4;
 d1,a _|_ c,b by A8, ANALMETR:61;
then  d,b _|_ a,c by A9, A6, A10, Th6;
hence  b,d _|_ a,c by ANALMETR:61; ::_thesis: verum
end;
now__::_thesis:_(_LIN_a,b,c_implies_b,d__|__a,c_)
A11: ( a = c implies b,d _|_ a,c ) by ANALMETR:58;
A12: ( b = c implies b,d _|_ a,c ) by A3, ANALMETR:61;
assume A13: LIN a,b,c ; ::_thesis: b,d _|_ a,c
 ( a = b implies b,d _|_ a,c ) by A4, ANALMETR:61;
hence  b,d _|_ a,c by A3, A4, A13, A11, A12, Th7; ::_thesis: verum
end;
hence  b,d _|_ a,c by A5; ::_thesis: verum
end;
hence  MS is Euclidean by Def1; ::_thesis: verum
end;
now__::_thesis:_(_MS_is_Euclidean_implies_MS_is_satisfying_3H_)
assume A14: MS is Euclidean ; ::_thesis: MS is satisfying_3H
now__::_thesis:_for_a,_b,_c_being_Element_of_MS_st_not_LIN_a,b,c_holds_
ex_d_being_Element_of_MS_st_
(_d,a__|__b,c_&_d,b__|__a,c_&_d,c__|__a,b_)
let a, b, c be Element of MS; ::_thesis: ( not LIN a,b,c implies ex d being Element of MS st
( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b ) )
assume  not LIN a,b,c ; ::_thesis: ex d being Element of MS st
( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b )
then consider d being Element of MS such that
A15: ( d,a _|_ b,c & d,b _|_ a,c ) by Th5;
take d = d; ::_thesis: ( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b )
 ( b,c _|_ a,d & c,a _|_ b,d ) by A15, ANALMETR:61;
then  c,d _|_ b,a by A14, Def1;
hence  ( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b ) by A15, ANALMETR:61; ::_thesis: verum
end;
hence  MS is satisfying_3H by CONAFFM:def_3; ::_thesis: verum
end;
hence  ( MS is Euclidean iff MS is satisfying_3H ) by A1; ::_thesis: verum
end;

theorem Th9: :: EUCLMETR:9
for MS being OrtAfPl holds
( MS is Homogeneous iff MS is satisfying_ODES )
proof
let MS be OrtAfPl; ::_thesis: ( MS is Homogeneous iff MS is satisfying_ODES )
 ( MS is satisfying_ODES iff for o, a, a1, b, b1, c, c1 being Element of MS st o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b holds
b,c _|_ b1,c1 ) by CONAFFM:def_4;
hence  ( MS is Homogeneous iff MS is satisfying_ODES ) by Def7; ::_thesis: verum
end;

Lm1:  for MS being OrtAfPl holds
( MS is satisfying_PAP iff Af MS is Pappian )
proof
let MS be OrtAfPl; ::_thesis: ( MS is satisfying_PAP iff Af MS is Pappian )
set AS = Af MS;
A1: now__::_thesis:_(_MS_is_satisfying_PAP_implies_Af_MS_is_Pappian_)
assume A2: MS is satisfying_PAP ; ::_thesis: Af MS is Pappian
now__::_thesis:_for_M,_N_being_Subset_of_(Af_MS)
for_o,_a,_b,_c,_a9,_b9,_c9_being_Element_of_(Af_MS)_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 M, N be Subset of (Af MS); ::_thesis: for o, a, b, c, a9, b9, c9 being Element of (Af MS) 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 (Af MS); ::_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
A3: ( M is being_line & N is being_line ) and
A4: M <> N and
A5: ( o in M & o in N ) and
A6: o <> a and
A7: ( o <> a9 & o <> b ) and
A8: ( o <> b9 & o <> c & o <> c9 & a in M ) and
A9: b in M and
A10: c in M and
A11: a9 in N and
A12: ( b9 in N & c9 in N ) and
A13: a,b9 // b,a9 and
A14: b,c9 // c,b9 ; ::_thesis: a,c9 // c,a9
reconsider M9 = M, N9 = N as Subset of MS by ANALMETR:42;
reconsider a1 = a, b1 = b, c1 = c, a19 = a9, b19 = b9, c19 = c9 as Element of MS by ANALMETR:35;
A15: b1,c19 // c1,b19 by A14, ANALMETR:36;
 a1,b19 // b1,a19 by A13, ANALMETR:36;
then A16: b1,a19 // a1,b19 by ANALMETR:59;
A17: ( M9 is being_line & N9 is being_line ) by A3, ANALMETR:43;
then  ( not a19 in M9 & not b1 in N9 ) by A4, A5, A7, A9, A11, CONMETR:5;
then  c1,a19 // a1,c19 by A2, A5, A6, A8, A9, A10, A11, A12, A17, A16, A15, CONMETR:def_2;
then  a1,c19 // c1,a19 by ANALMETR:59;
hence  a,c9 // c,a9 by ANALMETR:36; ::_thesis: verum
end;
hence  Af MS is Pappian by AFF_2:def_2; ::_thesis: verum
end;
now__::_thesis:_(_Af_MS_is_Pappian_implies_MS_is_satisfying_PAP_)
assume A18: Af MS is Pappian ; ::_thesis: MS is satisfying_PAP
now__::_thesis:_for_o,_a1,_a2,_a3,_b1,_b2,_b3_being_Element_of_MS
for_M,_N_being_Subset_of_the_carrier_of_MS_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
let o, a1, a2, a3, b1, b2, b3 be Element of MS; ::_thesis: for M, N being Subset of the carrier of MS 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
let M, N be Subset of the carrier of MS; ::_thesis: ( 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 implies a1,b2 // a2,b3 )
assume that
A19: ( M is being_line & N is being_line ) and
A20: ( 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 ) and
 o <> a3 and
A21: o <> b1 and
 o <> b2 and
A22: o <> b3 and
A23: a3,b2 // a2,b1 and
A24: a3,b3 // a1,b1 ; ::_thesis: a1,b2 // a2,b3
reconsider M9 = M, N9 = N as Subset of (Af MS) by ANALMETR:42;
reconsider a = a1, b = a2, c = a3, a9 = b1, b9 = b2, c9 = b3 as Element of (Af MS) by ANALMETR:35;
A25: c,c9 // a,a9 by A24, ANALMETR:36;
 a2,b1 // a3,b2 by A23, ANALMETR:59;
then A26: b,a9 // c,b9 by ANALMETR:36;
 ( M9 is being_line & N9 is being_line ) by A19, ANALMETR:43;
then  b,c9 // a,b9 by A18, A20, A21, A22, A26, A25, AFF_2:def_2;
then  a2,b3 // a1,b2 by ANALMETR:36;
hence  a1,b2 // a2,b3 by ANALMETR:59; ::_thesis: verum
end;
hence  MS is satisfying_PAP by CONMETR:def_2; ::_thesis: verum
end;
hence  ( MS is satisfying_PAP iff Af MS is Pappian ) by A1; ::_thesis: verum
end;

theorem Th10: :: EUCLMETR:10
for MS being OrtAfPl holds
( MS is Pappian iff MS is satisfying_PAP )
proof
let MS be OrtAfPl; ::_thesis: ( MS is Pappian iff MS is satisfying_PAP )
set AS = Af MS;
A1: now__::_thesis:_(_MS_is_satisfying_PAP_implies_MS_is_Pappian_)
assume  MS is satisfying_PAP ; ::_thesis: MS is Pappian
then  Af MS is Pappian by Lm1;
hence  MS is Pappian by Def2; ::_thesis: verum
end;
now__::_thesis:_(_MS_is_Pappian_implies_MS_is_satisfying_PAP_)
assume  MS is Pappian ; ::_thesis: MS is satisfying_PAP
then  Af MS is Pappian by Def2;
hence  MS is satisfying_PAP by Lm1; ::_thesis: verum
end;
hence  ( MS is Pappian iff MS is satisfying_PAP ) by A1; ::_thesis: verum
end;

Lm2:  for MS being OrtAfPl holds
( MS is satisfying_DES iff Af MS is Desarguesian )
proof
let MS be OrtAfPl; ::_thesis: ( MS is satisfying_DES iff Af MS is Desarguesian )
set AS = Af MS;
A1: now__::_thesis:_(_MS_is_satisfying_DES_implies_Af_MS_is_Desarguesian_)
assume A2: MS is satisfying_DES ; ::_thesis: Af MS is Desarguesian
now__::_thesis:_for_A,_P,_C_being_Subset_of_(Af_MS)
for_o,_a,_b,_c,_a9,_b9,_c9_being_Element_of_(Af_MS)_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 A, P, C be Subset of (Af MS); ::_thesis: for o, a, b, c, a9, b9, c9 being Element of (Af MS) 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 (Af MS); ::_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 )
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 and
A21: a,c // a9,c9 ; ::_thesis: b,c // b9,c9
now__::_thesis:_(_o_<>_a9_&_a_<>_a9_implies_b,c_//_b9,c9_)
reconsider o1 = o, a1 = a, b1 = b, c1 = c, a19 = a9, b19 = b9, c19 = c9 as Element of MS by ANALMETR:35;
assume that
A22: o <> a9 and
A23: a <> a9 ; ::_thesis: b,c // b9,c9
A24: ( a1,b1 // a19,b19 & a1,c1 // a19,c19 ) by A20, A21, ANALMETR:36;
A25: b <> b9 by A3, A4, A6, A7, A9, A10, A11, A15, A16, A18, A20, A23, AFF_4:9;
now__::_thesis:_not_LIN_b,b9,a
assume  LIN b,b9,a ; ::_thesis: contradiction
then  a in P by A11, A12, A16, A25, AFF_1:25;
hence  contradiction by A3, A4, A6, A9, A15, A16, A18, AFF_1:18; ::_thesis: verum
end;
then A26: not LIN b1,b19,a1 by ANALMETR:40;
 LIN o,a,a9 by A3, A9, A10, A15, AFF_1:21;
then A27: LIN o1,a1,a19 by ANALMETR:40;
now__::_thesis:_not_LIN_a,a9,c
assume  LIN a,a9,c ; ::_thesis: contradiction
then  c in A by A9, A10, A15, A23, AFF_1:25;
hence  contradiction by A3, A5, A8, A13, A15, A17, A19, AFF_1:18; ::_thesis: verum
end;
then A28: not LIN a1,a19,c1 by ANALMETR:40;
 LIN o,b,b9 by A4, A11, A12, A16, AFF_1:21;
then A29: LIN o1,b1,b19 by ANALMETR:40;
 LIN o,c,c9 by A5, A13, A14, A17, AFF_1:21;
then A30: LIN o1,c1,c19 by ANALMETR:40;
 ( o1 <> b19 & o1 <> c19 ) by A3, A4, A5, A6, A7, A8, A9, A10, A11, A13, A15, A16, A17, A18, A19, A20, A21, A22, AFF_4:8;
then  b1,c1 // b19,c19 by A2, A6, A7, A8, A22, A27, A29, A30, A24, A26, A28, CONAFFM:def_1;
hence  b,c // b9,c9 by ANALMETR:36; ::_thesis: verum
end;
hence  b,c // b9,c9 by A3, A4, A5, A6, A7, A8, A9, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A21, AFPROJ:50; ::_thesis: verum
end;
hence  Af MS is Desarguesian by AFF_2:def_4; ::_thesis: verum
end;
now__::_thesis:_(_Af_MS_is_Desarguesian_implies_MS_is_satisfying_DES_)
assume A31: Af MS is Desarguesian ; ::_thesis: MS is satisfying_DES
now__::_thesis:_for_o,_a,_a1,_b,_b1,_c,_c1_being_Element_of_MS_st_o_<>_a_&_o_<>_a1_&_o_<>_b_&_o_<>_b1_&_o_<>_c_&_o_<>_c1_&_not_LIN_b,b1,a_&_not_LIN_a,a1,c_&_LIN_o,a,a1_&_LIN_o,b,b1_&_LIN_o,c,c1_&_a,b_//_a1,b1_&_a,c_//_a1,c1_holds_
b,c_//_b1,c1
let o, a, a1, b, b1, c, c1 be Element of MS; ::_thesis: ( o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & not LIN b,b1,a & not LIN a,a1,c & LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1 & a,b // a1,b1 & a,c // a1,c1 implies b,c // b1,c1 )
assume that
A32: o <> a and
 o <> a1 and
A33: o <> b and
 o <> b1 and
A34: o <> c and
 o <> c1 and
A35: not LIN b,b1,a and
A36: not LIN a,a1,c and
A37: LIN o,a,a1 and
A38: LIN o,b,b1 and
A39: LIN o,c,c1 and
A40: ( a,b // a1,b1 & a,c // a1,c1 ) ; ::_thesis: b,c // b1,c1
reconsider o9 = o, a9 = a, b9 = b, c9 = c, a19 = a1, b19 = b1, c19 = c1 as Element of (Af MS) by ANALMETR:35;
 LIN o9,a9,a19 by A37, ANALMETR:40;
then consider A being Subset of (Af MS) such that
A41: A is being_line and
A42: o9 in A and
A43: a9 in A and
A44: a19 in A by AFF_1:21;
 LIN o9,c9,c19 by A39, ANALMETR:40;
then consider C being Subset of (Af MS) such that
A45: ( C is being_line & o9 in C ) and
A46: c9 in C and
A47: c19 in C by AFF_1:21;
A48: A <> C
proof
assume  A = C ; ::_thesis: contradiction
then  LIN a9,a19,c9 by A41, A43, A44, A46, AFF_1:21;
hence  contradiction by A36, ANALMETR:40; ::_thesis: verum
end;
 LIN o9,b9,b19 by A38, ANALMETR:40;
then consider P being Subset of (Af MS) such that
A49: P is being_line and
A50: o9 in P and
A51: ( b9 in P & b19 in P ) by AFF_1:21;
A52: A <> P
proof
assume  A = P ; ::_thesis: contradiction
then  LIN b9,b19,a9 by A43, A49, A51, AFF_1:21;
hence  contradiction by A35, ANALMETR:40; ::_thesis: verum
end;
 ( a9,b9 // a19,b19 & a9,c9 // a19,c19 ) by A40, ANALMETR:36;
then  b9,c9 // b19,c19 by A31, A32, A33, A34, A41, A42, A43, A44, A49, A50, A51, A45, A46, A47, A52, A48, AFF_2:def_4;
hence  b,c // b1,c1 by ANALMETR:36; ::_thesis: verum
end;
hence  MS is satisfying_DES by CONAFFM:def_1; ::_thesis: verum
end;
hence  ( MS is satisfying_DES iff Af MS is Desarguesian ) by A1; ::_thesis: verum
end;

theorem Th11: :: EUCLMETR:11
for MS being OrtAfPl holds
( MS is Desarguesian iff MS is satisfying_DES )
proof
let MS be OrtAfPl; ::_thesis: ( MS is Desarguesian iff MS is satisfying_DES )
set AS = Af MS;
A1: now__::_thesis:_(_MS_is_satisfying_DES_implies_MS_is_Desarguesian_)
assume  MS is satisfying_DES ; ::_thesis: MS is Desarguesian
then  Af MS is Desarguesian by Lm2;
hence  MS is Desarguesian by Def3; ::_thesis: verum
end;
now__::_thesis:_(_MS_is_Desarguesian_implies_MS_is_satisfying_DES_)
assume  MS is Desarguesian ; ::_thesis: MS is satisfying_DES
then  Af MS is Desarguesian by Def3;
hence  MS is satisfying_DES by Lm2; ::_thesis: verum
end;
hence  ( MS is Desarguesian iff MS is satisfying_DES ) by A1; ::_thesis: verum
end;

theorem :: EUCLMETR:12
for MS being OrtAfPl holds
( MS is Moufangian iff MS is satisfying_TDES )
proof
let MS be OrtAfPl; ::_thesis: ( MS is Moufangian iff MS is satisfying_TDES )
set AS = Af MS;
A1: now__::_thesis:_(_MS_is_satisfying_TDES_implies_MS_is_Moufangian_)
assume A2: MS is satisfying_TDES ; ::_thesis: MS is Moufangian
now__::_thesis:_for_K_being_Subset_of_(Af_MS)
for_o,_a,_b,_c,_a9,_b9,_c9_being_Element_of_(Af_MS)_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 (Af MS); ::_thesis: for o, a, b, c, a9, b9, c9 being Element of (Af MS) 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 (Af MS); ::_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
A3: K is being_line and
A4: o in K and
A5: c in K and
A6: c9 in K and
A7: not a in K and
A8: o <> c and
A9: a <> b and
A10: LIN o,a,a9 and
A11: LIN o,b,b9 and
A12: a,b // a9,b9 and
A13: a,c // a9,c9 and
A14: a,b // K ; ::_thesis: b,c // b9,c9
reconsider o1 = o, a1 = a, b1 = b, c1 = c, a19 = a9, b19 = b9, c19 = c9 as Element of MS by ANALMETR:35;
A15: ( o1 <> b1 & a1,c1 // a19,c19 ) by A4, A7, A13, A14, AFF_1:35, ANALMETR:36;
A16: not LIN o,a,c
proof
assume  LIN o,a,c ; ::_thesis: contradiction
then  LIN o,c,a by AFF_1:6;
hence  contradiction by A3, A4, A5, A7, A8, AFF_1:25; ::_thesis: verum
end;
A17: not LIN o,a,b
proof
set M = Line (a,b);
assume  LIN o,a,b ; ::_thesis: contradiction
then  LIN a,b,o by AFF_1:6;
then A18: o in Line (a,b) by AFF_1:def_2;
 ( a in Line (a,b) & Line (a,b) // K ) by A9, A14, AFF_1:15, AFF_1:def_5;
then  a in K by A4, A18, AFF_1:45;
hence  contradiction by A3, A4, A5, A16, AFF_1:21; ::_thesis: verum
end;
 a,b // o,c by A3, A4, A5, A8, A14, AFF_1:27;
then  b,a // o,c by AFF_1:4;
then A19: b1,a1 // o1,c1 by ANALMETR:36;
A20: ( LIN o1,a1,a19 & LIN o1,b1,b19 ) by A10, A11, ANALMETR:40;
 a1,b1 // a19,b19 by A12, ANALMETR:36;
then A21: b1,a1 // b19,a19 by ANALMETR:59;
A22: LIN o,c,c9 by A3, A4, A5, A6, AFF_1:21;
then A23: LIN o1,c1,c19 by ANALMETR:40;
A24: now__::_thesis:_(_a9_<>_o_implies_b,c_//_b9,c9_)
assume A25: a9 <> o ; ::_thesis: b,c // b9,c9
A26: now__::_thesis:_(_a_<>_a9_implies_b,c_//_b9,c9_)
assume A27: a <> a9 ; ::_thesis: b,c // b9,c9
A28: not LIN a1,a19,c1
proof
assume  LIN a1,a19,c1 ; ::_thesis: contradiction
then A29: LIN a,a9,c by ANALMETR:40;
 ( LIN a,a9,o & LIN a,a9,a ) by A10, AFF_1:6, AFF_1:7;
hence  contradiction by A16, A27, A29, AFF_1:8; ::_thesis: verum
end;
A30: not LIN a1,a19,b1
proof
assume  LIN a1,a19,b1 ; ::_thesis: contradiction
then A31: LIN a,a9,b by ANALMETR:40;
 ( LIN a,a9,o & LIN a,a9,a ) by A10, AFF_1:6, AFF_1:7;
hence  contradiction by A17, A27, A31, AFF_1:8; ::_thesis: verum
end;
 ( c,a // c9,a9 & not LIN o,c,a ) by A13, A16, AFF_1:4, AFF_1:6;
then A32: o1 <> c19 by A10, A25, AFF_1:55;
 ( b,a // b9,a9 & not LIN o,b,a ) by A12, A17, AFF_1:4, AFF_1:6;
then  o1 <> b19 by A10, A25, AFF_1:55;
then  b1,c1 // b19,c19 by A2, A4, A7, A8, A20, A23, A21, A19, A15, A25, A32, A28, A30, CONMETR:def_5;
hence  b,c // b9,c9 by ANALMETR:36; ::_thesis: verum
end;
now__::_thesis:_(_a_=_a9_implies_b,c_//_b9,c9_)
A33: LIN o,c,c by AFF_1:7;
assume A34: a = a9 ; ::_thesis: b,c // b9,c9
then  a,c // a9,c by AFF_1:2;
then A35: c = c9 by A10, A13, A22, A16, A33, AFF_1:56;
A36: LIN o,b,b by AFF_1:7;
 a,b // a9,b by A34, AFF_1:2;
then  b = b9 by A10, A11, A12, A17, A36, AFF_1:56;
hence  b,c // b9,c9 by A35, AFF_1:2; ::_thesis: verum
end;
hence  b,c // b9,c9 by A26; ::_thesis: verum
end;
now__::_thesis:_(_a9_=_o_implies_b,c_//_b9,c9_)
assume  a9 = o ; ::_thesis: b,c // b9,c9
then  ( b9 = o & c9 = o ) by A11, A12, A13, A22, A16, A17, AFF_1:55;
hence  b,c // b9,c9 by AFF_1:3; ::_thesis: verum
end;
hence  b,c // b9,c9 by A24; ::_thesis: verum
end;
then  Af MS is Moufangian by AFF_2:def_7;
hence  MS is Moufangian by Def5; ::_thesis: verum
end;
now__::_thesis:_(_MS_is_Moufangian_implies_MS_is_satisfying_TDES_)
assume  MS is Moufangian ; ::_thesis: MS is satisfying_TDES
then A37: Af MS is Moufangian by Def5;
now__::_thesis:_for_o,_a,_a1,_b,_b1,_c,_c1_being_Element_of_MS_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
let o, a, a1, b, b1, c, c1 be Element of MS; ::_thesis: ( 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 implies a,c // a1,c1 )
assume that
 o <> a and
 o <> a1 and
A38: o <> b and
 o <> b1 and
A39: o <> c and
 o <> c1 and
A40: not LIN b,b1,a and
A41: not LIN b,b1,c and
A42: LIN o,a,a1 and
A43: LIN o,b,b1 and
A44: LIN o,c,c1 and
A45: a,b // a1,b1 and
A46: a,b // o,c and
A47: b,c // b1,c1 ; ::_thesis: a,c // a1,c1
reconsider o9 = o, a9 = a, a19 = a1, b9 = b, b19 = b1, c9 = c, c19 = c1 as Element of (Af MS) by ANALMETR:35;
set K = Line (o9,c9);
A48: Line (o9,c9) is being_line by A39, AFF_1:def_3;
 a9,b9 // o9,c9 by A46, ANALMETR:36;
then  a9,b9 // Line (o9,c9) by A39, AFF_1:def_4;
then A49: b9,a9 // Line (o9,c9) by AFF_1:34;
 a9,b9 // a19,b19 by A45, ANALMETR:36;
then A50: b9,a9 // b19,a19 by AFF_1:4;
A51: c9 in Line (o9,c9) by AFF_1:15;
A52: ( LIN o9,a9,a19 & b9,c9 // b19,c19 ) by A42, A47, ANALMETR:36, ANALMETR:40;
A53: b9 <> a9 by A40, Th1;
A54: o9 in Line (o9,c9) by AFF_1:15;
A55: LIN o9,b9,b19 by A43, ANALMETR:40;
A56: not b9 in Line (o9,c9)
proof
assume A57: b9 in Line (o9,c9) ; ::_thesis: contradiction
then  b19 in Line (o9,c9) by A38, A48, A54, A55, AFF_1:25;
then  LIN b9,b19,c9 by A48, A51, A57, AFF_1:21;
hence  contradiction by A41, ANALMETR:40; ::_thesis: verum
end;
 LIN o9,c9,c19 by A44, ANALMETR:40;
then  c19 in Line (o9,c9) by A39, A48, A54, A51, AFF_1:25;
then  a9,c9 // a19,c19 by A37, A39, A48, A54, A51, A55, A56, A49, A50, A52, A53, AFF_2:def_7;
hence  a,c // a1,c1 by ANALMETR:36; ::_thesis: verum
end;
hence  MS is satisfying_TDES by CONMETR:def_5; ::_thesis: verum
end;
hence  ( MS is Moufangian iff MS is satisfying_TDES ) by A1; ::_thesis: verum
end;

Lm3:  for MS being OrtAfPl holds
( MS is satisfying_des iff Af MS is translational )
proof
let MS be OrtAfPl; ::_thesis: ( MS is satisfying_des iff Af MS is translational )
set AS = Af MS;
A1: now__::_thesis:_(_MS_is_satisfying_des_implies_Af_MS_is_translational_)
assume A2: MS is satisfying_des ; ::_thesis: Af MS is translational
now__::_thesis:_for_A,_P,_C_being_Subset_of_(Af_MS)
for_a,_b,_c,_a9,_b9,_c9_being_Element_of_(Af_MS)_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, P, C be Subset of (Af MS); ::_thesis: for a, b, c, a9, b9, c9 being Element of (Af MS) 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 (Af MS); ::_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
A3: A // P and
A4: A // C and
A5: a in A and
A6: a9 in A and
A7: b in P and
A8: b9 in P and
A9: c in C and
A10: c9 in C and
A11: A is being_line and
A12: P is being_line and
A13: C is being_line and
A14: A <> P and
A15: A <> C and
A16: a,b // a9,b9 and
A17: a,c // a9,c9 ; ::_thesis: b,c // b9,c9
A18: not a in C by A4, A5, A15, AFF_1:45;
A19: now__::_thesis:_(_a_<>_a9_implies_b,c_//_b9,c9_)
reconsider aa = a, a1 = a9, bb = b, b1 = b9, cc = c, c1 = c9 as Element of MS by ANALMETR:35;
 a,a9 // b,b9 by A3, A5, A6, A7, A8, AFF_1:39;
then A20: aa,a1 // bb,b1 by ANALMETR:36;
 a,a9 // c,c9 by A4, A5, A6, A9, A10, AFF_1:39;
then A21: aa,a1 // cc,c1 by ANALMETR:36;
assume A22: a <> a9 ; ::_thesis: b,c // b9,c9
A23: not LIN aa,a1,bb
proof
assume  LIN aa,a1,bb ; ::_thesis: contradiction
then  LIN a,a9,b by ANALMETR:40;
then  b in A by A5, A6, A11, A22, AFF_1:25;
hence  contradiction by A3, A7, A14, AFF_1:45; ::_thesis: verum
end;
A24: not LIN aa,a1,cc
proof
assume  LIN aa,a1,cc ; ::_thesis: contradiction
then  LIN a,a9,c by ANALMETR:40;
then  c in A by A5, A6, A11, A22, AFF_1:25;
hence  contradiction by A4, A9, A15, AFF_1:45; ::_thesis: verum
end;
 ( aa,bb // a1,b1 & aa,cc // a1,c1 ) by A16, A17, ANALMETR:36;
then  bb,cc // b1,c1 by A2, A23, A24, A20, A21, CONMETR:def_8;
hence  b,c // b9,c9 by ANALMETR:36; ::_thesis: verum
end;
A25: not a in P by A3, A5, A14, AFF_1:45;
now__::_thesis:_(_a_=_a9_implies_b,c_//_b9,c9_)
assume A26: a = a9 ; ::_thesis: b,c // b9,c9
then  LIN a,c,c9 by A17, AFF_1:def_1;
then  LIN c,c9,a by AFF_1:6;
then A27: c = c9 by A9, A10, A13, A18, AFF_1:25;
 LIN a,b,b9 by A16, A26, AFF_1:def_1;
then  LIN b,b9,a by AFF_1:6;
then  b = b9 by A7, A8, A12, A25, AFF_1:25;
hence  b,c // b9,c9 by A27, AFF_1:2; ::_thesis: verum
end;
hence  b,c // b9,c9 by A19; ::_thesis: verum
end;
hence  Af MS is translational by AFF_2:def_11; ::_thesis: verum
end;
now__::_thesis:_(_Af_MS_is_translational_implies_MS_is_satisfying_des_)
assume A28: Af MS is translational ; ::_thesis: MS is satisfying_des
now__::_thesis:_for_a,_a1,_b,_b1,_c,_c1_being_Element_of_MS_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
let a, a1, b, b1, c, c1 be Element of MS; ::_thesis: ( 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 implies b,c // b1,c1 )
assume that
A29: ( not LIN a,a1,b & not LIN a,a1,c ) and
A30: a,a1 // b,b1 and
A31: a,a1 // c,c1 and
A32: ( a,b // a1,b1 & a,c // a1,c1 ) ; ::_thesis: b,c // b1,c1
reconsider a9 = a, a19 = a1, b9 = b, b19 = b1, c9 = c, c19 = c1 as Element of (Af MS) by ANALMETR:35;
A33: a9,a19 // b9,b19 by A30, ANALMETR:36;
A34: ( a9,b9 // a19,b19 & a9,c9 // a19,c19 ) by A32, ANALMETR:36;
A35: a9,a19 // c9,c19 by A31, ANALMETR:36;
set A = Line (a9,a19);
A36: ( not a9,a19 // a9,b9 & not a9,a19 // a9,c9 )
proof
assume  ( a9,a19 // a9,b9 or a9,a19 // a9,c9 ) ; ::_thesis: contradiction
then  ( a,a1 // a,b or a,a1 // a,c ) by ANALMETR:36;
hence  contradiction by A29, ANALMETR:def_10; ::_thesis: verum
end;
then A37: a9 <> a19 by AFF_1:3;
then A38: Line (a9,a19) is being_line by AFF_1:def_3;
then consider C being Subset of (Af MS) such that
A39: c9 in C and
A40: Line (a9,a19) // C by AFF_1:49;
A41: C is being_line by A40, AFF_1:36;
A42: ( a9 in Line (a9,a19) & a19 in Line (a9,a19) ) by AFF_1:15;
then A43: Line (a9,a19) <> C by A36, A38, A39, AFF_1:51;
A44: a9,a19 // Line (a9,a19) by A38, A42, AFF_1:23;
then  a9,a19 // C by A40, AFF_1:43;
then  c9,c19 // C by A35, A37, AFF_1:32;
then A45: c19 in C by A39, A41, AFF_1:23;
consider P being Subset of (Af MS) such that
A46: b9 in P and
A47: Line (a9,a19) // P by A38, AFF_1:49;
A48: P is being_line by A47, AFF_1:36;
 a9,a19 // P by A44, A47, AFF_1:43;
then  b9,b19 // P by A33, A37, AFF_1:32;
then A49: b19 in P by A46, A48, AFF_1:23;
 Line (a9,a19) <> P by A36, A38, A42, A46, AFF_1:51;
then  b9,c9 // b19,c19 by A28, A34, A38, A42, A46, A47, A39, A40, A48, A41, A49, A45, A43, AFF_2:def_11;
hence  b,c // b1,c1 by ANALMETR:36; ::_thesis: verum
end;
hence  MS is satisfying_des by CONMETR:def_8; ::_thesis: verum
end;
hence  ( MS is satisfying_des iff Af MS is translational ) by A1; ::_thesis: verum
end;

theorem :: EUCLMETR:13
for MS being OrtAfPl holds
( MS is translation iff MS is satisfying_des )
proof
let MS be OrtAfPl; ::_thesis: ( MS is translation iff MS is satisfying_des )
set AS = Af MS;
A1: now__::_thesis:_(_MS_is_satisfying_des_implies_MS_is_translation_)
assume  MS is satisfying_des ; ::_thesis: MS is translation
then  Af MS is translational by Lm3;
hence  MS is translation by Def6; ::_thesis: verum
end;
now__::_thesis:_(_MS_is_translation_implies_MS_is_satisfying_des_)
assume  MS is translation ; ::_thesis: MS is satisfying_des
then  Af MS is translational by Def6;
hence  MS is satisfying_des by Lm3; ::_thesis: verum
end;
hence  ( MS is translation iff MS is satisfying_des ) by A1; ::_thesis: verum
end;

theorem Th14: :: EUCLMETR:14
for MS being OrtAfPl st MS is Homogeneous holds
MS is Desarguesian
proof
let MS be OrtAfPl; ::_thesis: ( MS is Homogeneous implies MS is Desarguesian )
assume  MS is Homogeneous ; ::_thesis: MS is Desarguesian
then  MS is satisfying_ODES by Th9;
then  MS is satisfying_DES by CONAFFM:1;
hence  MS is Desarguesian by Th11; ::_thesis: verum
end;

theorem Th15: :: EUCLMETR:15
for MS being OrtAfPl st MS is Euclidean & MS is Desarguesian holds
MS is Pappian
proof
let MS be OrtAfPl; ::_thesis: ( MS is Euclidean & MS is Desarguesian implies MS is Pappian )
assume  ( MS is Euclidean & MS is Desarguesian ) ; ::_thesis: MS is Pappian
then  ( MS is satisfying_3H & MS is satisfying_DES ) by Th8, Th11;
then  MS is satisfying_PAP by CONMETR:13, CONMETR:15;
hence  MS is Pappian by Th10; ::_thesis: verum
end;


theorem Th16: :: EUCLMETR:16
for MS being OrtAfPl
for o, c, c1, a, a1, a2 being Element of MS st not LIN o,c,a & o <> c1 & o,c _|_ o,c1 & o,a _|_ o,a1 & o,a _|_ o,a2 & c,a _|_ c1,a1 & c,a _|_ c1,a2 holds
a1 = a2
proof
let MS be OrtAfPl; ::_thesis: for o, c, c1, a, a1, a2 being Element of MS st not LIN o,c,a & o <> c1 & o,c _|_ o,c1 & o,a _|_ o,a1 & o,a _|_ o,a2 & c,a _|_ c1,a1 & c,a _|_ c1,a2 holds
a1 = a2
let o, c, c1, a, a1, a2 be Element of MS; ::_thesis: ( not LIN o,c,a & o <> c1 & o,c _|_ o,c1 & o,a _|_ o,a1 & o,a _|_ o,a2 & c,a _|_ c1,a1 & c,a _|_ c1,a2 implies a1 = a2 )
assume that
A1: not LIN o,c,a and
A2: ( o <> c1 & o,c _|_ o,c1 ) and
A3: ( o,a _|_ o,a1 & o,a _|_ o,a2 ) and
A4: ( c,a _|_ c1,a1 & c,a _|_ c1,a2 ) ; ::_thesis: a1 = a2
reconsider o9 = o, a19 = a1, a29 = a2, c19 = c1 as Element of (Af MS) by ANALMETR:35;
assume A5: a1 <> a2 ; ::_thesis: contradiction
 o <> a by A1, Th1;
then  o,a1 // o,a2 by A3, ANALMETR:63;
then  o9,a19 // o9,a29 by ANALMETR:36;
then  LIN o9,a19,a29 by AFF_1:def_1;
then A6: LIN a19,a29,o9 by AFF_1:6;
 a <> c by A1, Th1;
then  c1,a1 // c1,a2 by A4, ANALMETR:63;
then  c19,a19 // c19,a29 by ANALMETR:36;
then  LIN c19,a19,a29 by AFF_1:def_1;
then A7: LIN a19,a29,c19 by AFF_1:6;
 LIN a19,a29,a29 by AFF_1:7;
then  LIN o9,c19,a29 by A5, A6, A7, AFF_1:8;
then  o9,c19 // o9,a29 by AFF_1:def_1;
then  o,c1 // o,a2 by ANALMETR:36;
then A8: o,c _|_ o,a2 by A2, ANALMETR:62;
 LIN a19,a29,a19 by AFF_1:7;
then  LIN o9,c19,a19 by A5, A6, A7, AFF_1:8;
then  o9,c19 // o9,a19 by AFF_1:def_1;
then  o,c1 // o,a1 by ANALMETR:36;
then A9: o,c _|_ o,a1 by A2, ANALMETR:62;
 ( o <> a1 or o <> a2 ) by A5;
then  o,c // o,a by A3, A9, A8, ANALMETR:63;
hence  contradiction by A1, ANALMETR:def_10; ::_thesis: verum
end;

theorem :: EUCLMETR:17
for MS being OrtAfPl
for o, c, c1, a being Element of MS st not LIN o,c,a holds
ex a1 being Element of MS st
( o,a _|_ o,a1 & c,a _|_ c1,a1 )
proof
let MS be OrtAfPl; ::_thesis: for o, c, c1, a being Element of MS st not LIN o,c,a holds
ex a1 being Element of MS st
( o,a _|_ o,a1 & c,a _|_ c1,a1 )
let o, c, c1, a be Element of MS; ::_thesis: ( not LIN o,c,a implies ex a1 being Element of MS st
( o,a _|_ o,a1 & c,a _|_ c1,a1 ) )
assume A1: not LIN o,c,a ; ::_thesis: ex a1 being Element of MS st
( o,a _|_ o,a1 & c,a _|_ c1,a1 )
set X = Line (c,a);
set Y = Line (o,a);
 c <> a by A1, Th1;
then A2: Line (c,a) is being_line by ANALMETR:def_12;
then consider X9 being Subset of MS such that
A3: c1 in X9 and
A4: Line (c,a) _|_ X9 by CONMETR:3;
 o <> a by A1, Th1;
then  Line (o,a) is being_line by ANALMETR:def_12;
then consider Y9 being Subset of MS such that
A5: o in Y9 and
A6: Line (o,a) _|_ Y9 by CONMETR:3;
reconsider X1 = X9, Y1 = Y9 as Subset of (Af MS) by ANALMETR:42;
 Y9 is being_line by A6, ANALMETR:44;
then A7: Y1 is being_line by ANALMETR:43;
reconsider o9 = o, c9 = c, a9 = a as Element of (Af MS) by ANALMETR:35;
A8: Line (c,a) = Line (c9,a9) by ANALMETR:41;
then A9: a in Line (c,a) by AFF_1:15;
 Line (o,a) = Line (o9,a9) by ANALMETR:41;
then A10: ( o in Line (o,a) & a in Line (o,a) ) by AFF_1:15;
A11: c in Line (c,a) by A8, AFF_1:15;
 not X9 // Y9
proof
reconsider X1 = Line (c,a), Y1 = Line (o,a) as Subset of the carrier of (Af MS) by ANALMETR:42;
assume  X9 // Y9 ; ::_thesis: contradiction
then  X9 _|_ Line (o,a) by A6, ANALMETR:52;
then  Line (c,a) // Line (o,a) by A4, ANALMETR:65;
then  X1 // Y1 by ANALMETR:46;
then A12: o in Line (c,a) by A9, A10, AFF_1:45;
 a in Line (c,a) by A8, AFF_1:15;
hence  contradiction by A1, A2, A11, A12, CONMETR:4; ::_thesis: verum
end;
then A13: not X1 // Y1 by ANALMETR:46;
 X9 is being_line by A4, ANALMETR:44;
then  X1 is being_line by ANALMETR:43;
then consider a19 being Element of (Af MS) such that
A14: ( a19 in X1 & a19 in Y1 ) by A7, A13, AFF_1:58;
reconsider a1 = a19 as Element of MS by ANALMETR:35;
take  a1 ; ::_thesis: ( o,a _|_ o,a1 & c,a _|_ c1,a1 )
thus  ( o,a _|_ o,a1 & c,a _|_ c1,a1 ) by A3, A4, A5, A6, A11, A9, A10, A14, ANALMETR:56; ::_thesis: verum
end;

Lm4:  for V being RealLinearSpace
for u, v, y being VECTOR of V holds
( (u - y) - (v - y) = u - v & (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 & (u + y) - (v + y) = u - v )
let u, v, y be VECTOR of V; ::_thesis: ( (u - y) - (v - y) = u - v & (u + y) - (v + y) = u - v )
thus (u - y) - (v - y) = (u - y) + (y - v) by RLVECT_1:33
.= u - v by ANALOAF:1 ; ::_thesis: (u + y) - (v + y) = u - v
thus (u + y) - (v + y) = (u - (- y)) - (v + y) by RLVECT_1:17
.= (u - (- y)) - (v - (- y)) by RLVECT_1:17
.= (u - (- y)) + ((- y) - v) by RLVECT_1:33
.= u - v by ANALOAF:1 ; ::_thesis: verum
end;

Lm5:  for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
for a, b, c being Real holds
( PProJ (w,y,((a * w) + (b * y)),(((c * b) * w) + ((- (c * a)) * y))) = 0 & (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y )
proof
let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V st Gen w,y holds
for a, b, c being Real holds
( PProJ (w,y,((a * w) + (b * y)),(((c * b) * w) + ((- (c * a)) * y))) = 0 & (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y )
let w, y be VECTOR of V; ::_thesis: ( Gen w,y implies for a, b, c being Real holds
( PProJ (w,y,((a * w) + (b * y)),(((c * b) * w) + ((- (c * a)) * y))) = 0 & (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y ) )
assume A1: Gen w,y ; ::_thesis: for a, b, c being Real holds
( PProJ (w,y,((a * w) + (b * y)),(((c * b) * w) + ((- (c * a)) * y))) = 0 & (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y )
let a, b, c be Real; ::_thesis: ( PProJ (w,y,((a * w) + (b * y)),(((c * b) * w) + ((- (c * a)) * y))) = 0 & (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y )
A2: ( pr2 (w,y,((a * w) + (b * y))) = b & pr2 (w,y,(((c * b) * w) + ((- (c * a)) * y))) = - (c * a) ) by A1, GEOMTRAP:def_5;
 ( pr1 (w,y,((a * w) + (b * y))) = a & pr1 (w,y,(((c * b) * w) + ((- (c * a)) * y))) = c * b ) by A1, GEOMTRAP:def_4;
hence  PProJ (w,y,((a * w) + (b * y)),(((c * b) * w) + ((- (c * a)) * y))) = (a * (b * c)) + (b * (- (c * a))) by A2, GEOMTRAP:def_6
.= 0 ;
::_thesis: (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y
hence  (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y by A1, GEOMTRAP:32; ::_thesis: verum
end;

theorem Th18: :: EUCLMETR:18
for V being RealLinearSpace
for w, y, u, v being VECTOR of V
for a, b being Real st Gen w,y & 0. V <> u & 0. V <> v & u,v are_Ort_wrt w,y & u = (a * w) + (b * y) holds
ex c being Real st
( c <> 0 & v = ((c * b) * w) + ((- (c * a)) * y) )
proof
let V be RealLinearSpace; ::_thesis: for w, y, u, v being VECTOR of V
for a, b being Real st Gen w,y & 0. V <> u & 0. V <> v & u,v are_Ort_wrt w,y & u = (a * w) + (b * y) holds
ex c being Real st
( c <> 0 & v = ((c * b) * w) + ((- (c * a)) * y) )
let w, y, u, v be VECTOR of V; ::_thesis: for a, b being Real st Gen w,y & 0. V <> u & 0. V <> v & u,v are_Ort_wrt w,y & u = (a * w) + (b * y) holds
ex c being Real st
( c <> 0 & v = ((c * b) * w) + ((- (c * a)) * y) )
let a, b be Real; ::_thesis: ( Gen w,y & 0. V <> u & 0. V <> v & u,v are_Ort_wrt w,y & u = (a * w) + (b * y) implies ex c being Real st
( c <> 0 & v = ((c * b) * w) + ((- (c * a)) * y) ) )
assume that
A1: Gen w,y and
A2: 0. V <> u and
A3: 0. V <> v and
A4: u,v are_Ort_wrt w,y and
A5: u = (a * w) + (b * y) ; ::_thesis: ex c being Real st
( c <> 0 & v = ((c * b) * w) + ((- (c * a)) * y) )
set v9 = (b * w) + ((- a) * y);
 (b * w) + ((- a) * y) = ((1 * b) * w) + ((- (1 * a)) * y) ;
then  u,(b * w) + ((- a) * y) are_Ort_wrt w,y by A1, A5, Lm5;
then consider a1, b1 being Real such that
A6: a1 * v = b1 * ((b * w) + ((- a) * y)) and
A7: ( a1 <> 0 or b1 <> 0 ) by A1, A2, A4, ANALMETR:9;
A8: now__::_thesis:_not_a1_=_0
assume A9: a1 = 0 ; ::_thesis: contradiction
then  0. V = b1 * ((b * w) + ((- a) * y)) by A6, RLVECT_1:10;
then  (b * w) + ((- a) * y) = 0. V by A7, A9, RLVECT_1:11;
then  ( b = 0 & - a = 0 ) by A1, ANALMETR:def_1;
then u = (0. V) + (0 * y) by A5, RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
hence  contradiction by A2; ::_thesis: verum
end;
take c = (a1 ") * b1; ::_thesis: ( c <> 0 & v = ((c * b) * w) + ((- (c * a)) * y) )
A10: now__::_thesis:_not_b1_=_0
assume A11: b1 = 0 ; ::_thesis: contradiction
then  0. V = a1 * v by A6, RLVECT_1:10;
hence  contradiction by A3, A7, A11, RLVECT_1:11; ::_thesis: verum
end;
now__::_thesis:_not_c_=_0
assume  c = 0 ; ::_thesis: contradiction
then  a1 " = 0 by A10, XCMPLX_1:6;
hence  contradiction by A8, XCMPLX_1:202; ::_thesis: verum
end;
hence  c <> 0 ; ::_thesis: v = ((c * b) * w) + ((- (c * a)) * y)
thus v = (a1 ") * (b1 * ((b * w) + ((- a) * y))) by A6, A8, ANALOAF:5
.= c * ((b * w) + ((- a) * y)) by RLVECT_1:def_7
.= (c * (b * w)) + (c * ((- a) * y)) by RLVECT_1:def_5
.= ((c * b) * w) + (c * ((- a) * y)) by RLVECT_1:def_7
.= ((c * b) * w) + ((c * (- a)) * y) by RLVECT_1:def_7
.= ((c * b) * w) + ((- (c * a)) * y) ; ::_thesis: verum
end;

theorem Th19: :: EUCLMETR:19
for V being RealLinearSpace
for w, y, u, v being VECTOR of V st Gen w,y & 0. V <> u & 0. V <> v & u,v are_Ort_wrt w,y holds
ex c being Real st
for a, b being Real holds
( (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y & ((a * w) + (b * y)) - u,(((c * b) * w) + ((- (c * a)) * y)) - v are_Ort_wrt w,y )
proof
let V be RealLinearSpace; ::_thesis: for w, y, u, v being VECTOR of V st Gen w,y & 0. V <> u & 0. V <> v & u,v are_Ort_wrt w,y holds
ex c being Real st
for a, b being Real holds
( (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y & ((a * w) + (b * y)) - u,(((c * b) * w) + ((- (c * a)) * y)) - v are_Ort_wrt w,y )
let w, y, u, v be VECTOR of V; ::_thesis: ( Gen w,y & 0. V <> u & 0. V <> v & u,v are_Ort_wrt w,y implies ex c being Real st
for a, b being Real holds
( (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y & ((a * w) + (b * y)) - u,(((c * b) * w) + ((- (c * a)) * y)) - v are_Ort_wrt w,y ) )
assume that
A1: Gen w,y and
A2: ( 0. V <> u & 0. V <> v ) and
A3: u,v are_Ort_wrt w,y ; ::_thesis: ex c being Real st
for a, b being Real holds
( (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y & ((a * w) + (b * y)) - u,(((c * b) * w) + ((- (c * a)) * y)) - v are_Ort_wrt w,y )
consider a1, a2 being Real such that
A4: u = (a1 * w) + (a2 * y) by A1, ANALMETR:def_1;
consider c being Real such that
 c <> 0 and
A5: v = ((c * a2) * w) + ((- (c * a1)) * y) by A1, A2, A3, A4, Th18;
take  c ; ::_thesis: for a, b being Real holds
( (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y & ((a * w) + (b * y)) - u,(((c * b) * w) + ((- (c * a)) * y)) - v are_Ort_wrt w,y )
let a, b be Real; ::_thesis: ( (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y & ((a * w) + (b * y)) - u,(((c * b) * w) + ((- (c * a)) * y)) - v are_Ort_wrt w,y )
set u9 = (a * w) + (b * y);
set v9 = ((c * b) * w) + ((- (c * a)) * y);
A6: ( pr1 (w,y,((a * w) + (b * y))) = a & pr2 (w,y,((a * w) + (b * y))) = b ) by A1, GEOMTRAP:def_4, GEOMTRAP:def_5;
A7: ( pr1 (w,y,(((c * b) * w) + ((- (c * a)) * y))) = c * b & pr2 (w,y,(((c * b) * w) + ((- (c * a)) * y))) = - (c * a) ) by A1, GEOMTRAP:def_4, GEOMTRAP:def_5;
 ( pr1 (w,y,u) = a1 & pr2 (w,y,u) = a2 ) by A1, A4, GEOMTRAP:def_4, GEOMTRAP:def_5;
then A8: PProJ (w,y,u,(((c * b) * w) + ((- (c * a)) * y))) = (a1 * (c * b)) + (a2 * (- (c * a))) by A7, GEOMTRAP:def_6;
 ( pr1 (w,y,v) = c * a2 & pr2 (w,y,v) = - (c * a1) ) by A1, A5, GEOMTRAP:def_4, GEOMTRAP:def_5;
then A9: PProJ (w,y,((a * w) + (b * y)),v) = ((c * a2) * a) + ((- (c * a1)) * b) by A6, GEOMTRAP:def_6;
thus  (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y by A1, Lm5; ::_thesis: ((a * w) + (b * y)) - u,(((c * b) * w) + ((- (c * a)) * y)) - v are_Ort_wrt w,y
PProJ (w,y,(((a * w) + (b * y)) - u),((((c * b) * w) + ((- (c * a)) * y)) - v)) = (PProJ (w,y,(((a * w) + (b * y)) - u),(((c * b) * w) + ((- (c * a)) * y)))) - (PProJ (w,y,(((a * w) + (b * y)) - u),v)) by A1, GEOMTRAP:30
.= ((PProJ (w,y,((a * w) + (b * y)),(((c * b) * w) + ((- (c * a)) * y)))) - (PProJ (w,y,u,(((c * b) * w) + ((- (c * a)) * y))))) - (PProJ (w,y,(((a * w) + (b * y)) - u),v)) by A1, GEOMTRAP:30
.= (0 - (PProJ (w,y,u,(((c * b) * w) + ((- (c * a)) * y))))) - (PProJ (w,y,(((a * w) + (b * y)) - u),v)) by A1, Lm5
.= (- (PProJ (w,y,u,(((c * b) * w) + ((- (c * a)) * y))))) - ((PProJ (w,y,((a * w) + (b * y)),v)) - (PProJ (w,y,u,v))) by A1, GEOMTRAP:30
.= (- (PProJ (w,y,u,(((c * b) * w) + ((- (c * a)) * y))))) - ((PProJ (w,y,((a * w) + (b * y)),v)) - 0) by A1, A3, GEOMTRAP:32
.= (- 1) * ((PProJ (w,y,u,(((c * b) * w) + ((- (c * a)) * y)))) + (PProJ (w,y,((a * w) + (b * y)),v))) ;
hence  ((a * w) + (b * y)) - u,(((c * b) * w) + ((- (c * a)) * y)) - v are_Ort_wrt w,y by A1, A8, A9, GEOMTRAP:32; ::_thesis: verum
end;

Lm6:  for V being RealLinearSpace
for w, y being VECTOR of V
for a, b, c, d being Real holds ((a * w) + (b * y)) - ((c * w) + (d * y)) = ((a - c) * w) + ((b - d) * y)
proof
let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V
for a, b, c, d being Real holds ((a * w) + (b * y)) - ((c * w) + (d * y)) = ((a - c) * w) + ((b - d) * y)
let w, y be VECTOR of V; ::_thesis: for a, b, c, d being Real holds ((a * w) + (b * y)) - ((c * w) + (d * y)) = ((a - c) * w) + ((b - d) * y)
let a, b, c, d be Real; ::_thesis: ((a * w) + (b * y)) - ((c * w) + (d * y)) = ((a - c) * w) + ((b - d) * y)
thus ((a * w) + (b * y)) - ((c * w) + (d * y)) = (b * y) + ((a * w) - ((c * w) + (d * y))) by RLVECT_1:def_3
.= (b * y) + (((a * w) - (c * w)) - (d * y)) by RLVECT_1:27
.= (b * y) + (((a - c) * w) - (d * y)) by RLVECT_1:35
.= (((a - c) * w) + (b * y)) - (d * y) by RLVECT_1:def_3
.= ((a - c) * w) + ((b * y) - (d * y)) by RLVECT_1:def_3
.= ((a - c) * w) + ((b - d) * y) by RLVECT_1:35 ; ::_thesis: verum
end;

Lm7:  for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
for a, b, c, d being Real st (a * w) + (c * y) = (b * w) + (d * y) holds
( a = b & c = d )
proof
let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V st Gen w,y holds
for a, b, c, d being Real st (a * w) + (c * y) = (b * w) + (d * y) holds
( a = b & c = d )
let w, y be VECTOR of V; ::_thesis: ( Gen w,y implies for a, b, c, d being Real st (a * w) + (c * y) = (b * w) + (d * y) holds
( a = b & c = d ) )
assume A1: Gen w,y ; ::_thesis: for a, b, c, d being Real st (a * w) + (c * y) = (b * w) + (d * y) holds
( a = b & c = d )
let a, b, c, d be Real; ::_thesis: ( (a * w) + (c * y) = (b * w) + (d * y) implies ( a = b & c = d ) )
assume  (a * w) + (c * y) = (b * w) + (d * y) ; ::_thesis: ( a = b & c = d )
then  0. V = ((a * w) + (c * y)) - ((b * w) + (d * y)) by RLVECT_1:15
.= ((a - b) * w) + ((c - d) * y) by Lm6 ;
then  ( (- b) + a = 0 & (- d) + c = 0 ) by A1, ANALMETR:def_1;
hence  ( a = b & c = d ) ; ::_thesis: verum
end;

theorem Th20: :: EUCLMETR:20
for MS being OrtAfPl
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y & MS = AMSpace (V,w,y) holds
MS is satisfying_LIN
proof
let MS be OrtAfPl; ::_thesis: for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y & MS = AMSpace (V,w,y) holds
MS is satisfying_LIN
let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V st Gen w,y & MS = AMSpace (V,w,y) holds
MS is satisfying_LIN
let w, y be VECTOR of V; ::_thesis: ( Gen w,y & MS = AMSpace (V,w,y) implies MS is satisfying_LIN )
assume that
A1: Gen w,y and
A2: MS = AMSpace (V,w,y) ; ::_thesis: MS is satisfying_LIN
now__::_thesis:_for_o,_a,_a1,_b,_b1,_c,_c1_being_Element_of_MS_st_o_<>_a_&_o_<>_a1_&_o_<>_b_&_o_<>_b1_&_o_<>_c_&_o_<>_c1_&_a_<>_b_&_o,c__|__o,c1_&_o,a__|__o,a1_&_o,b__|__o,b1_&_not_LIN_o,c,a_&_LIN_o,a,b_&_LIN_o,a1,b1_&_a,c__|__a1,c1_&_b,c__|__b1,c1_holds_
a,a1_//_b,b1
let o, a, a1, b, b1, c, c1 be Element of MS; ::_thesis: ( o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & a <> b & o,c _|_ o,c1 & o,a _|_ o,a1 & o,b _|_ o,b1 & not LIN o,c,a & LIN o,a,b & LIN o,a1,b1 & a,c _|_ a1,c1 & b,c _|_ b1,c1 implies a,a1 // b,b1 )
assume that
A3: o <> a and
 o <> a1 and
A4: o <> b and
 o <> b1 and
A5: o <> c and
A6: o <> c1 and
 a <> b and
A7: o,c _|_ o,c1 and
A8: o,a _|_ o,a1 and
A9: o,b _|_ o,b1 and
A10: not LIN o,c,a and
A11: LIN o,a,b and
 LIN o,a1,b1 and
A12: a,c _|_ a1,c1 and
A13: b,c _|_ b1,c1 ; ::_thesis: a,a1 // b,b1
reconsider q = o, u1 = a, u2 = b, u3 = c, v3 = c1 as VECTOR of V by A2, ANALMETR:19;
consider A1, A2 being Real such that
A14: u1 - q = (A1 * w) + (A2 * y) by A1, ANALMETR:def_1;
A15: not LIN o,c,b
proof
reconsider o9 = o, a9 = a, b9 = b, c9 = c as Element of (Af MS) by ANALMETR:35;
assume  LIN o,c,b ; ::_thesis: contradiction
then  LIN o9,c9,b9 by ANALMETR:40;
then A16: LIN o9,b9,c9 by AFF_1:6;
 LIN o9,a9,b9 by A11, ANALMETR:40;
then A17: LIN o9,b9,a9 by AFF_1:6;
 LIN o9,b9,o9 by AFF_1:7;
then  LIN o9,c9,a9 by A4, A16, A17, AFF_1:8;
hence  contradiction by A10, ANALMETR:40; ::_thesis: verum
end;
 q,u3,q,v3 are_Ort_wrt w,y by A2, A7, ANALMETR:21;
then A18: u3 - q,v3 - q are_Ort_wrt w,y by ANALMETR:def_3;
 ( u3 - q <> 0. V & v3 - q <> 0. V ) by A5, A6, RLVECT_1:21;
then consider r being Real such that
A19: for a9, b9 being Real holds
( (a9 * w) + (b9 * y),((r * b9) * w) + ((- (r * a9)) * y) are_Ort_wrt w,y & ((a9 * w) + (b9 * y)) - (u3 - q),(((r * b9) * w) + ((- (r * a9)) * y)) - (v3 - q) are_Ort_wrt w,y ) by A1, A18, Th19;
 o,a // o,b by A11, ANALMETR:def_10;
then  q,u1 '||' q,u2 by A2, GEOMTRAP:4;
then  ( q,u1 // q,u2 or q,u1 // u2,q ) by GEOMTRAP:def_1;
then consider a9, b9 being Real such that
A20: a9 * (u1 - q) = b9 * (u2 - q) and
A21: ( a9 <> 0 or b9 <> 0 ) by ANALMETR:14;
consider B1, B2 being Real such that
A22: u2 - q = (B1 * w) + (B2 * y) by A1, ANALMETR:def_1;
set s = (b9 ") * a9;
A23: u1 - q <> 0. V by A3, RLVECT_1:21;
now__::_thesis:_not_b9_=_0
assume A24: b9 = 0 ; ::_thesis: contradiction
then  0. V = a9 * (u1 - q) by A20, RLVECT_1:10;
hence  contradiction by A23, A21, A24, RLVECT_1:11; ::_thesis: verum
end;
then A25: u2 - q = (b9 ") * (a9 * (u1 - q)) by A20, ANALOAF:5
.= ((b9 ") * a9) * (u1 - q) by RLVECT_1:def_7 ;
then (B1 * w) + (B2 * y) = (((b9 ") * a9) * (A1 * w)) + (((b9 ") * a9) * (A2 * y)) by A14, A22, RLVECT_1:def_5
.= ((((b9 ") * a9) * A1) * w) + (((b9 ") * a9) * (A2 * y)) by RLVECT_1:def_7
.= ((((b9 ") * a9) * A1) * w) + ((((b9 ") * a9) * A2) * y) by RLVECT_1:def_7 ;
then A26: ( B1 = ((b9 ") * a9) * A1 & B2 = ((b9 ") * a9) * A2 ) by A1, Lm7;
set v19 = (((r * A2) * w) + ((- (r * A1)) * y)) + q;
set v29 = (((r * B2) * w) + ((- (r * B1)) * y)) + q;
reconsider a19 = (((r * A2) * w) + ((- (r * A1)) * y)) + q, b19 = (((r * B2) * w) + ((- (r * B1)) * y)) + q as Element of MS by A2, ANALMETR:19;
A27: ((((r * B2) * w) + ((- (r * B1)) * y)) + q) - q = ((r * B2) * w) + ((- (r * B1)) * y) by RLSUB_2:61
.= ((r * B2) * w) + ((r * B1) * (- y)) by RLVECT_1:24
.= ((r * (((b9 ") * a9) * A2)) * w) - ((r * (((b9 ") * a9) * A1)) * y) by A26, RLVECT_1:25
.= (r * ((((b9 ") * a9) * A2) * w)) - ((r * (((b9 ") * a9) * A1)) * y) by RLVECT_1:def_7
.= (r * ((((b9 ") * a9) * A2) * w)) - (r * ((((b9 ") * a9) * A1) * y)) by RLVECT_1:def_7
.= r * (((((b9 ") * a9) * A2) * w) - ((((b9 ") * a9) * A1) * y)) by RLVECT_1:34
.= r * ((((b9 ") * a9) * (A2 * w)) - ((((b9 ") * a9) * A1) * y)) by RLVECT_1:def_7
.= r * ((((b9 ") * a9) * (A2 * w)) - (((b9 ") * a9) * (A1 * y))) by RLVECT_1:def_7
.= r * (((b9 ") * a9) * ((A2 * w) - (A1 * y))) by RLVECT_1:34
.= (((b9 ") * a9) * r) * ((A2 * w) - (A1 * y)) by RLVECT_1:def_7
.= ((b9 ") * a9) * (r * ((A2 * w) - (A1 * y))) by RLVECT_1:def_7
.= ((b9 ") * a9) * ((r * (A2 * w)) - (r * (A1 * y))) by RLVECT_1:34
.= ((b9 ") * a9) * (((r * A2) * w) - (r * (A1 * y))) by RLVECT_1:def_7
.= ((b9 ") * a9) * (((r * A2) * w) + (- ((r * A1) * y))) by RLVECT_1:def_7
.= ((b9 ") * a9) * (((r * A2) * w) + ((r * A1) * (- y))) by RLVECT_1:25
.= ((b9 ") * a9) * (((r * A2) * w) + ((- (r * A1)) * y)) by RLVECT_1:24
.= ((b9 ") * a9) * (((((r * A2) * w) + ((- (r * A1)) * y)) + q) - q) by RLSUB_2:61 ;
A28: ((((r * B2) * w) + ((- (r * B1)) * y)) + q) - q = ((r * B2) * w) + ((- (r * B1)) * y) by RLSUB_2:61;
then  u2 - q,((((r * B2) * w) + ((- (r * B1)) * y)) + q) - q are_Ort_wrt w,y by A19, A22;
then  q,u2,q,(((r * B2) * w) + ((- (r * B1)) * y)) + q are_Ort_wrt w,y by ANALMETR:def_3;
then A29: o,b _|_ o,b19 by A2, ANALMETR:21;
1 * (u2 - ((((r * B2) * w) + ((- (r * B1)) * y)) + q)) = u2 - ((((r * B2) * w) + ((- (r * B1)) * y)) + q) by RLVECT_1:def_8
.= (((b9 ") * a9) * (u1 - q)) - (((b9 ") * a9) * (((((r * A2) * w) + ((- (r * A1)) * y)) + q) - q)) by A25, A27, Lm4
.= ((b9 ") * a9) * ((u1 - q) - (((((r * A2) * w) + ((- (r * A1)) * y)) + q) - q)) by RLVECT_1:34
.= ((b9 ") * a9) * (u1 - ((((r * A2) * w) + ((- (r * A1)) * y)) + q)) by Lm4 ;
then  ( (((r * A2) * w) + ((- (r * A1)) * y)) + q,u1 // (((r * B2) * w) + ((- (r * B1)) * y)) + q,u2 or (((r * A2) * w) + ((- (r * A1)) * y)) + q,u1 // u2,(((r * B2) * w) + ((- (r * B1)) * y)) + q ) by ANALMETR:14;
then  (((r * A2) * w) + ((- (r * A1)) * y)) + q,u1 '||' (((r * B2) * w) + ((- (r * B1)) * y)) + q,u2 by GEOMTRAP:def_1;
then A30: a19,a // b19,b by A2, GEOMTRAP:4;
A31: ((((r * A2) * w) + ((- (r * A1)) * y)) + q) - q = ((r * A2) * w) + ((- (r * A1)) * y) by RLSUB_2:61;
then  u1 - q,((((r * A2) * w) + ((- (r * A1)) * y)) + q) - q are_Ort_wrt w,y by A19, A14;
then  q,u1,q,(((r * A2) * w) + ((- (r * A1)) * y)) + q are_Ort_wrt w,y by ANALMETR:def_3;
then A32: o,a _|_ o,a19 by A2, ANALMETR:21;
 ( (u2 - q) - (u3 - q) = u2 - u3 & (((((r * B2) * w) + ((- (r * B1)) * y)) + q) - q) - (v3 - q) = ((((r * B2) * w) + ((- (r * B1)) * y)) + q) - v3 ) by Lm4;
then  u2 - u3,((((r * B2) * w) + ((- (r * B1)) * y)) + q) - v3 are_Ort_wrt w,y by A19, A22, A28;
then  u3,u2,v3,(((r * B2) * w) + ((- (r * B1)) * y)) + q are_Ort_wrt w,y by ANALMETR:def_3;
then A33: c,b _|_ c1,b19 by A2, ANALMETR:21;
 c,b _|_ c1,b1 by A13, ANALMETR:61;
then A34: b1 = b19 by A6, A7, A9, A15, A29, A33, Th16;
 ( (u1 - q) - (u3 - q) = u1 - u3 & (((((r * A2) * w) + ((- (r * A1)) * y)) + q) - q) - (v3 - q) = ((((r * A2) * w) + ((- (r * A1)) * y)) + q) - v3 ) by Lm4;
then  u1 - u3,((((r * A2) * w) + ((- (r * A1)) * y)) + q) - v3 are_Ort_wrt w,y by A19, A14, A31;
then  u3,u1,v3,(((r * A2) * w) + ((- (r * A1)) * y)) + q are_Ort_wrt w,y by ANALMETR:def_3;
then A35: c,a _|_ c1,a19 by A2, ANALMETR:21;
 c,a _|_ c1,a1 by A12, ANALMETR:61;
then  a1 = a19 by A6, A7, A8, A10, A32, A35, Th16;
hence  a,a1 // b,b1 by A34, A30, ANALMETR:59; ::_thesis: verum
end;
hence  MS is satisfying_LIN by CONAFFM:def_5; ::_thesis: verum
end;

theorem Th21: :: EUCLMETR:21
for MS being OrtAfPl
for o, a, a1, b, b1, c, c1 being Element of MS st o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b & o = a1 holds
b,c _|_ b1,c1
proof
let MS be OrtAfPl; ::_thesis: for o, a, a1, b, b1, c, c1 being Element of MS st o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b & o = a1 holds
b,c _|_ b1,c1
let o, a, a1, b, b1, c, c1 be Element of MS; ::_thesis: ( o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b & o = a1 implies b,c _|_ b1,c1 )
assume that
A1: o,b _|_ o,b1 and
A2: o,c _|_ o,c1 and
A3: a,b _|_ a1,b1 and
A4: a,c _|_ a1,c1 and
A5: not o,c // o,a and
A6: not o,a // o,b and
A7: o = a1 ; ::_thesis: b,c _|_ b1,c1
A8: o = c1
proof
assume  o <> c1 ; ::_thesis: contradiction
then  a,c // o,c by A2, A4, A7, ANALMETR:63;
then  c,a // c,o by ANALMETR:59;
then  LIN c,a,o by ANALMETR:def_10;
then  LIN o,c,a by Th4;
hence  contradiction by A5, ANALMETR:def_10; ::_thesis: verum
end;
 o = b1
proof
assume  o <> b1 ; ::_thesis: contradiction
then  a,b // o,b by A1, A3, A7, ANALMETR:63;
then  b,a // b,o by ANALMETR:59;
then  LIN b,a,o by ANALMETR:def_10;
then  LIN o,a,b by Th4;
hence  contradiction by A6, ANALMETR:def_10; ::_thesis: verum
end;
hence  b,c _|_ b1,c1 by A8, ANALMETR:58; ::_thesis: verum
end;

theorem Th22: :: EUCLMETR:22
for MS being OrtAfPl
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y & MS = AMSpace (V,w,y) holds
MS is Homogeneous
proof
let MS be OrtAfPl; ::_thesis: for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y & MS = AMSpace (V,w,y) holds
MS is Homogeneous
let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V st Gen w,y & MS = AMSpace (V,w,y) holds
MS is Homogeneous
let w, y be VECTOR of V; ::_thesis: ( Gen w,y & MS = AMSpace (V,w,y) implies MS is Homogeneous )
assume that
A1: Gen w,y and
A2: MS = AMSpace (V,w,y) ; ::_thesis: MS is Homogeneous
now__::_thesis:_for_o,_a,_a1,_b,_b1,_c,_c1_being_Element_of_MS_st_o,a__|__o,a1_&_o,b__|__o,b1_&_o,c__|__o,c1_&_a,b__|__a1,b1_&_a,c__|__a1,c1_&_not_o,c_//_o,a_&_not_o,a_//_o,b_holds_
b,c__|__b1,c1
let o, a, a1, b, b1, c, c1 be Element of MS; ::_thesis: ( o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b implies b,c _|_ b1,c1 )
assume that
A3: o,a _|_ o,a1 and
A4: o,b _|_ o,b1 and
A5: o,c _|_ o,c1 and
A6: a,b _|_ a1,b1 and
A7: a,c _|_ a1,c1 and
A8: ( not o,c // o,a & not o,a // o,b ) ; ::_thesis: b,c _|_ b1,c1
reconsider q = o, u1 = a, u2 = b, u3 = c, v1 = a1 as VECTOR of V by A2, ANALMETR:19;
A9: ( not LIN o,a,b & not LIN o,a,c )
proof
assume  ( LIN o,a,b or LIN o,a,c ) ; ::_thesis: contradiction
then  ( o,a // o,b or o,a // o,c ) by ANALMETR:def_10;
hence  contradiction by A8, ANALMETR:59; ::_thesis: verum
end;
then A10: o <> a by Th1;
now__::_thesis:_(_o_<>_a1_implies_b,c__|__b1,c1_)
 q,u1,q,v1 are_Ort_wrt w,y by A2, A3, ANALMETR:21;
then A11: u1 - q,v1 - q are_Ort_wrt w,y by ANALMETR:def_3;
A12: u1 - q <> 0. V by A10, RLVECT_1:21;
assume A13: o <> a1 ; ::_thesis: b,c _|_ b1,c1
then  v1 - q <> 0. V by RLVECT_1:21;
then consider r being Real such that
A14: for a9, b9 being Real holds
( (a9 * w) + (b9 * y),((r * b9) * w) + ((- (r * a9)) * y) are_Ort_wrt w,y & ((a9 * w) + (b9 * y)) - (u1 - q),(((r * b9) * w) + ((- (r * a9)) * y)) - (v1 - q) are_Ort_wrt w,y ) by A1, A11, A12, Th19;
consider B1, B2 being Real such that
A15: u2 - q = (B1 * w) + (B2 * y) by A1, ANALMETR:def_1;
consider A1, A2 being Real such that
A16: u3 - q = (A1 * w) + (A2 * y) by A1, ANALMETR:def_1;
set v39 = (((r * A2) * w) + ((- (r * A1)) * y)) + q;
set v29 = (((r * B2) * w) + ((- (r * B1)) * y)) + q;
reconsider c19 = (((r * A2) * w) + ((- (r * A1)) * y)) + q, b19 = (((r * B2) * w) + ((- (r * B1)) * y)) + q as Element of MS by A2, ANALMETR:19;
A17: ((((r * B2) * w) + ((- (r * B1)) * y)) + q) - q = ((r * B2) * w) + ((- (r * B1)) * y) by RLSUB_2:61;
 ( (u2 - q) - (u1 - q) = u2 - u1 & (((((r * B2) * w) + ((- (r * B1)) * y)) + q) - q) - (v1 - q) = ((((r * B2) * w) + ((- (r * B1)) * y)) + q) - v1 ) by Lm4;
then  u2 - u1,((((r * B2) * w) + ((- (r * B1)) * y)) + q) - v1 are_Ort_wrt w,y by A14, A15, A17;
then  u1,u2,v1,(((r * B2) * w) + ((- (r * B1)) * y)) + q are_Ort_wrt w,y by ANALMETR:def_3;
then A18: a,b _|_ a1,b19 by A2, ANALMETR:21;
 u2 - q,((((r * B2) * w) + ((- (r * B1)) * y)) + q) - q are_Ort_wrt w,y by A14, A15, A17;
then  q,u2,q,(((r * B2) * w) + ((- (r * B1)) * y)) + q are_Ort_wrt w,y by ANALMETR:def_3;
then  o,b _|_ o,b19 by A2, ANALMETR:21;
then A19: b1 = b19 by A3, A4, A6, A9, A13, A18, Th16;
A20: ((((r * A2) * w) + ((- (r * A1)) * y)) + q) - q = ((r * A2) * w) + ((- (r * A1)) * y) by RLSUB_2:61;
u3 - u2 = ((A1 * w) + (A2 * y)) - ((B1 * w) + (B2 * y)) by A16, A15, Lm4
.= ((A1 - B1) * w) + ((A2 - B2) * y) by Lm6 ;
then A21: ( pr1 (w,y,(u3 - u2)) = A1 - B1 & pr2 (w,y,(u3 - u2)) = A2 - B2 ) by A1, GEOMTRAP:def_4, GEOMTRAP:def_5;
((((r * A2) * w) + ((- (r * A1)) * y)) + q) - ((((r * B2) * w) + ((- (r * B1)) * y)) + q) = (((r * A2) * w) + ((r * (- A1)) * y)) - (((r * B2) * w) + ((- (r * B1)) * y)) by Lm4
.= (((r * A2) - (r * B2)) * w) + (((r * (- A1)) - (r * (- B1))) * y) by Lm6
.= ((r * (A2 - B2)) * w) + ((r * (B1 - A1)) * y) ;
then  ( pr1 (w,y,(((((r * A2) * w) + ((- (r * A1)) * y)) + q) - ((((r * B2) * w) + ((- (r * B1)) * y)) + q))) = r * (A2 - B2) & pr2 (w,y,(((((r * A2) * w) + ((- (r * A1)) * y)) + q) - ((((r * B2) * w) + ((- (r * B1)) * y)) + q))) = r * (B1 - A1) ) by A1, GEOMTRAP:def_4, GEOMTRAP:def_5;
then  PProJ (w,y,(u3 - u2),(((((r * A2) * w) + ((- (r * A1)) * y)) + q) - ((((r * B2) * w) + ((- (r * B1)) * y)) + q))) = ((A1 - B1) * (r * (A2 - B2))) + ((A2 - B2) * (r * (B1 - A1))) by A21, GEOMTRAP:def_6
.= 0 ;
then  u3 - u2,((((r * A2) * w) + ((- (r * A1)) * y)) + q) - ((((r * B2) * w) + ((- (r * B1)) * y)) + q) are_Ort_wrt w,y by A1, GEOMTRAP:32;
then A22: u2,u3,(((r * B2) * w) + ((- (r * B1)) * y)) + q,(((r * A2) * w) + ((- (r * A1)) * y)) + q are_Ort_wrt w,y by ANALMETR:def_3;
 ( (u3 - q) - (u1 - q) = u3 - u1 & (((((r * A2) * w) + ((- (r * A1)) * y)) + q) - q) - (v1 - q) = ((((r * A2) * w) + ((- (r * A1)) * y)) + q) - v1 ) by Lm4;
then  u3 - u1,((((r * A2) * w) + ((- (r * A1)) * y)) + q) - v1 are_Ort_wrt w,y by A14, A16, A20;
then  u1,u3,v1,(((r * A2) * w) + ((- (r * A1)) * y)) + q are_Ort_wrt w,y by ANALMETR:def_3;
then A23: a,c _|_ a1,c19 by A2, ANALMETR:21;
 u3 - q,((((r * A2) * w) + ((- (r * A1)) * y)) + q) - q are_Ort_wrt w,y by A14, A16, A20;
then  q,u3,q,(((r * A2) * w) + ((- (r * A1)) * y)) + q are_Ort_wrt w,y by ANALMETR:def_3;
then  o,c _|_ o,c19 by A2, ANALMETR:21;
then  c1 = c19 by A3, A5, A7, A9, A13, A23, Th16;
hence  b,c _|_ b1,c1 by A2, A19, A22, ANALMETR:21; ::_thesis: verum
end;
hence  b,c _|_ b1,c1 by A4, A5, A6, A7, A8, Th21; ::_thesis: verum
end;
hence  MS is Homogeneous by Def7; ::_thesis: verum
end;

registration
clusterV42() OrtAfSp-like OrtAfPl-like Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous for ParOrtStr ;
existence
 ex b1 being OrtAfPl st
( b1 is Euclidean & b1 is Pappian & b1 is Desarguesian & b1 is Homogeneous & b1 is translation & b1 is Fanoian & b1 is Moufangian )
proof
consider V being RealLinearSpace such that
A1: ex w, y being VECTOR of V st Gen w,y by ANALMETR:3;
consider w, y being VECTOR of V such that
A2: Gen w,y by A1;
reconsider MS = AMSpace (V,w,y) as OrtAfPl by A2, ANALMETR:34;
A3: MS is satisfying_3H by A2, Th20, CONAFFM:6;
 for a, b being Real st (a * w) + (b * y) = 0. V holds
( a = 0 & b = 0 ) by A2, ANALMETR:def_1;
then reconsider OAS = OASpace V as OAffinSpace by ANALOAF:26;
take  MS ; ::_thesis: ( MS is Euclidean & MS is Pappian & MS is Desarguesian & MS is Homogeneous & MS is translation & MS is Fanoian & MS is Moufangian )
A4: Af MS = Lambda OAS by ANALMETR:20;
then A5: ( Af MS is Moufangian & Af MS is translational ) by PAPDESAF:16, PAPDESAF:17;
 ( Af MS is Pappian & Af MS is Desarguesian ) by A4, PAPDESAF:13, PAPDESAF:14;
hence  ( MS is Euclidean & MS is Pappian & MS is Desarguesian & MS is Homogeneous & MS is translation & MS is Fanoian & MS is Moufangian ) by A2, A3, A4, A5, Def2, Def3, Def4, Def5, Def6, Th8, Th22; ::_thesis: verum
end;
end;

registration
clusterV42() OrtAfSp-like Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous for ParOrtStr ;
existence
 ex b1 being OrtAfSp st
( b1 is Euclidean & b1 is Pappian & b1 is Desarguesian & b1 is Homogeneous & b1 is translation & b1 is Fanoian & b1 is Moufangian )
proof
set MS = the Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl;
 ( the Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl is Euclidean & the Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl is Pappian & the Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl is Desarguesian & the Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl is Homogeneous & the Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl is translation & the Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl is Fanoian & the Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl is Moufangian ) ;
hence  ex b1 being OrtAfSp st
( b1 is Euclidean & b1 is Pappian & b1 is Desarguesian & b1 is Homogeneous & b1 is translation & b1 is Fanoian & b1 is Moufangian ) ; ::_thesis: verum
end;
end;

theorem :: EUCLMETR:23
for MS being OrtAfPl
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y & MS = AMSpace (V,w,y) holds
MS is Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl
proof
let MS be OrtAfPl; ::_thesis: for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y & MS = AMSpace (V,w,y) holds
MS is Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl
let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V st Gen w,y & MS = AMSpace (V,w,y) holds
MS is Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl
let w, y be VECTOR of V; ::_thesis: ( Gen w,y & MS = AMSpace (V,w,y) implies MS is Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl )
assume that
A1: Gen w,y and
A2: MS = AMSpace (V,w,y) ; ::_thesis: MS is Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl
reconsider MS9 = AMSpace (V,w,y) as OrtAfPl by A2;
A3: MS9 is satisfying_3H by A1, Th20, CONAFFM:6;
 for a, b being Real st (a * w) + (b * y) = 0. V holds
( a = 0 & b = 0 ) by A1, ANALMETR:def_1;
then reconsider OAS = OASpace V as OAffinSpace by ANALOAF:26;
A4: Af MS9 = Lambda OAS by ANALMETR:20;
then A5: ( Af MS9 is Moufangian & Af MS9 is translational ) by PAPDESAF:16, PAPDESAF:17;
 ( Af MS9 is Pappian & Af MS9 is Desarguesian ) by A4, PAPDESAF:13, PAPDESAF:14;
hence  MS is Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl by A1, A2, A3, A4, A5, Def2, Def3, Def4, Def5, Def6, Th8, Th22; ::_thesis: verum
end;

registration
let MS be Pappian OrtAfPl;
cluster Af MS ->  Pappian ;
correctness
coherence
Af MS is Pappian ;
by Def2;
end;

registration
let MS be Desarguesian OrtAfPl;
cluster Af MS ->  Desarguesian ;
correctness
coherence
Af MS is Desarguesian ;
by Def3;
end;

registration
let MS be Moufangian OrtAfPl;
cluster Af MS ->  Moufangian ;
correctness
coherence
Af MS is Moufangian ;
by Def5;
end;

registration
let MS be translation OrtAfPl;
cluster Af MS ->  translational ;
correctness
coherence
Af MS is translational ;
by Def6;
end;

registration
let MS be Fanoian OrtAfPl;
cluster Af MS ->  Fanoian ;
correctness
coherence
Af MS is Fanoian ;
by Def4;
end;

registration
let MS be Homogeneous OrtAfPl;
cluster Af MS ->  Desarguesian ;
correctness
coherence
Af MS is Desarguesian ;
proof
 MS is Desarguesian by Th14;
hence  Af MS is Desarguesian ; ::_thesis: verum
end;
end;

registration
let MS be Euclidean Desarguesian OrtAfPl;
cluster Af MS ->  Pappian ;
correctness
coherence
Af MS is Pappian ;
proof
 MS is Pappian by Th15;
hence  Af MS is Pappian ; ::_thesis: verum
end;
end;

registration
let MS be Pappian OrtAfSp;
cluster Af MS ->  Pappian ;
correctness
coherence
Af MS is Pappian ;
by Def2;
end;

registration
let MS be Desarguesian OrtAfSp;
cluster Af MS ->  Desarguesian ;
correctness
coherence
Af MS is Desarguesian ;
by Def3;
end;

registration
let MS be Moufangian OrtAfSp;
cluster Af MS ->  Moufangian ;
correctness
coherence
Af MS is Moufangian ;
by Def5;
end;

registration
let MS be translation OrtAfSp;
cluster Af MS ->  translational ;
correctness
coherence
Af MS is translational ;
by Def6;
end;

registration
let MS be Fanoian OrtAfSp;
cluster Af MS ->  Fanoian ;
correctness
coherence
Af MS is Fanoian ;
by Def4;
end;