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 Th11;
for A, P, C being Subset of (Lambda OAP)
for o, a, b, c, a', b', c' being Element of (Lambda OAP) st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c'
proof
let A,
P,
C be
Subset of
(Lambda OAP);
:: thesis: for o, a, b, c, a', b', c' being Element of (Lambda OAP) st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c'let o,
a,
b,
c,
a',
b',
c' be
Element of
(Lambda OAP);
:: thesis: ( o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' implies b,c // b',c' )
reconsider o1 =
o,
a1 =
a,
b1 =
b,
c1 =
c,
a1' =
a',
b1' =
b',
c1' =
c' as
Element of
OAP by Th2;
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:
a' in A
and A11:
b in P
and A12:
b' in P
and A13:
c in C
and A14:
c' 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 // a',
b' &
a,
c // a',
c' )
;
:: thesis: b,c // b',c'
LIN o,
b,
b'
by A4, A11, A12, A16, AFF_1:33;
then A21:
LIN o1,
b1,
b1'
by Th3;
A22:
( not
LIN o1,
a1,
b1 & not
LIN o1,
a1,
c1 )
proof
A23:
now assume
LIN o,
a,
c
;
:: thesis: 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:33;
X = C
by A5, A8, A13, A17, A24, A26, AFF_1:30;
hence
contradiction
by A3, A6, A9, A15, A19, A24, A25, AFF_1:30;
:: thesis: verum end;
A27:
now assume
LIN o,
a,
b
;
:: thesis: 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:33;
X = P
by A4, A7, A11, A16, A28, A30, AFF_1:30;
hence
contradiction
by A3, A6, A9, A15, A18, A28, A29, AFF_1:30;
:: thesis: verum end;
assume
(
LIN o1,
a1,
b1 or
LIN o1,
a1,
c1 )
;
:: thesis: contradiction
hence
contradiction
by A27, A23, Th3;
:: thesis: verum
end;
LIN o,
c,
c'
by A5, A13, A14, A17, AFF_1:33;
then A31:
LIN o1,
c1,
c1'
by Th3;
A32:
(
a1,
b1 '||' a1',
b1' &
a1,
c1 '||' a1',
c1' )
by A20, DIRAF:45;
A33:
now assume A34:
a1,
o1 // o1,
a1'
;
:: thesis: b,c // b',c'then A35:
(
a1,
b1 // b1',
a1' &
a1,
c1 // c1',
a1' )
by A21, A31, A22, A32, Th12;
(
b1,
o1 // o1,
b1' &
c1,
o1 // o1,
c1' )
by A21, A31, A22, A32, A34, Th12;
then
b1,
c1 // c1',
b1'
by A1, A22, A34, A35, Def16;
then
b1,
c1 '||' b1',
c1'
by DIRAF:def 4;
hence
b,
c // b',
c'
by DIRAF:45;
:: thesis: verum end;
A36:
now assume A37:
o1,
a1 // o1,
a1'
;
:: thesis: b,c // b',c'then A38:
(
a1,
b1 // a1',
b1' &
a1,
c1 // a1',
c1' )
by A21, A31, A22, A32, Th13;
(
o1,
b1 // o1,
b1' &
o1,
c1 // o1,
c1' )
by A21, A31, A22, A32, A37, Th13;
then
b1,
c1 // b1',
c1'
by A2, A22, A37, A38, Def15;
then
b1,
c1 '||' b1',
c1'
by DIRAF:def 4;
hence
b,
c // b',
c'
by DIRAF:45;
:: thesis: verum end;
LIN o,
a,
a'
by A3, A9, A10, A15, AFF_1:33;
then
LIN o1,
a1,
a1'
by Th3;
then
(
Mid o1,
a1,
a1' or
Mid a1,
o1,
a1' or
Mid o1,
a1',
a1 )
by DIRAF:35;
hence
b,
c // b',
c'
by A33, A36, DIRAF:11, DIRAF:def 3;
:: thesis: verum
end;
hence
Lambda OAP is Desarguesian
by AFF_2:def 4; :: thesis: verum