let OAP be OAffinSpace; ( OAP is satisfying_DES_1 implies Lambda OAP is Desarguesian )
set AP = Lambda OAP;
assume A1:
OAP is satisfying_DES_1
; 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);
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,c9let o,
a,
b,
c,
a9,
b9,
c9 be
Element of
(Lambda OAP);
( 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 )
;
b,c // b9,c9
LIN o,
b,
b9
by A4, A11, A12, A16, AFF_1:21;
then A21:
o1,
b1,
b19 are_collinear
by Th2;
A22:
( not
o1,
a1,
b1 are_collinear & not
o1,
a1,
c1 are_collinear )
proof
A23:
now not LIN o,a,cassume
LIN o,
a,
c
;
contradictionthen 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;
verum end;
A27:
now not LIN o,a,bassume
LIN o,
a,
b
;
contradictionthen 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;
verum end;
assume
(
o1,
a1,
b1 are_collinear or
o1,
a1,
c1 are_collinear )
;
contradiction
hence
contradiction
by A27, A23, Th2;
verum
end;
LIN o,
c,
c9
by A5, A13, A14, A17, AFF_1:21;
then A31:
o1,
c1,
c19 are_collinear
by Th2;
A32:
(
a1,
b1 '||' a19,
b19 &
a1,
c1 '||' a19,
c19 )
by A20, DIRAF:38;
A33:
now ( a1,o1 // o1,a19 implies b,c // b9,c9 )assume A34:
a1,
o1 // o1,
a19
;
b,c // b9,c9then 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;
then
b1,
c1 '||' b19,
c19
by DIRAF:def 4;
hence
b,
c // b9,
c9
by DIRAF:38;
verum end;
A36:
now ( o1,a1 // o1,a19 implies b,c // b9,c9 )assume A37:
o1,
a1 // o1,
a19
;
b,c // b9,c9then 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;
then
b1,
c1 '||' b19,
c19
by DIRAF:def 4;
hence
b,
c // b9,
c9
by DIRAF:38;
verum end;
LIN o,
a,
a9
by A3, A9, A10, A15, AFF_1:21;
then
o1,
a1,
a19 are_collinear
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;
verum
end;
hence
Lambda OAP is Desarguesian
by AFF_2:def 4; verum