let MS be OrtAfPl; ( MS is satisfying_DES iff AffinStruct(# the carrier of MS, the CONGR of MS #) is Desarguesian )
set AS = AffinStruct(# the carrier of MS, the CONGR of MS #);
A1:
now ( MS is satisfying_DES implies AffinStruct(# the carrier of MS, the CONGR of MS #) is Desarguesian )assume A2:
MS is
satisfying_DES
;
AffinStruct(# the carrier of MS, the CONGR of MS #) is Desarguesian now for A, P, C being Subset of AffinStruct(# the carrier of MS, the CONGR of MS #)
for o, a, b, c, a9, b9, c9 being Element of AffinStruct(# the carrier of MS, the CONGR of 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,c9let A,
P,
C be
Subset of
AffinStruct(# the
carrier of
MS, the
CONGR of
MS #);
for o, a, b, c, a9, b9, c9 being Element of AffinStruct(# the carrier of MS, the CONGR of 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,c9let o,
a,
b,
c,
a9,
b9,
c9 be
Element of
AffinStruct(# the
carrier of
MS, the
CONGR of
MS #);
( 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
;
b,c // b9,c9now ( 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 ;
assume that A22:
o <> a9
and A23:
a <> a9
;
b,c // b9,c9A24:
(
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 not LIN b,b9,aassume
LIN b,
b9,
a
;
contradictionthen
a in P
by A11, A12, A16, A25, AFF_1:25;
hence
contradiction
by A3, A4, A6, A9, A15, A16, A18, AFF_1:18;
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 not LIN a,a9,cassume
LIN a,
a9,
c
;
contradictionthen
c in A
by A9, A10, A15, A23, AFF_1:25;
hence
contradiction
by A3, A5, A8, A13, A15, A17, A19, AFF_1:18;
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;
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;
verum end; hence
AffinStruct(# the
carrier of
MS, the
CONGR of
MS #) is
Desarguesian
by AFF_2:def 4;
verum end;
now ( AffinStruct(# the carrier of MS, the CONGR of MS #) is Desarguesian implies MS is satisfying_DES )assume A31:
AffinStruct(# the
carrier of
MS, the
CONGR of
MS #) is
Desarguesian
;
MS is satisfying_DES now 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,c1let o,
a,
a1,
b,
b1,
c,
c1 be
Element of
MS;
( 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 )
;
b,c // b1,c1reconsider o9 =
o,
a9 =
a,
b9 =
b,
c9 =
c,
a19 =
a1,
b19 =
b1,
c19 =
c1 as
Element of
AffinStruct(# the
carrier of
MS, the
CONGR of
MS #) ;
LIN o9,
a9,
a19
by A37, ANALMETR:40;
then consider A being
Subset of
AffinStruct(# the
carrier of
MS, the
CONGR of
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
AffinStruct(# the
carrier of
MS, the
CONGR of
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
LIN o9,
b9,
b19
by A38, ANALMETR:40;
then consider P being
Subset of
AffinStruct(# the
carrier of
MS, the
CONGR of
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
(
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;
verum end; hence
MS is
satisfying_DES
by CONAFFM:def 1;
verum end;
hence
( MS is satisfying_DES iff AffinStruct(# the carrier of MS, the CONGR of MS #) is Desarguesian )
by A1; verum