let AP be AffinPlane; ( AP is Desarguesian iff AP is satisfying_DES_1 )
hereby ( AP is satisfying_DES_1 implies AP is Desarguesian )
assume A54:
AP is
Desarguesian
;
AP is satisfying_DES_1 thus
AP is
satisfying_DES_1
verumproof
let A be
Subset of
AP;
AFF_2:def 5 for P, C being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & 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 & b,c // b9,c9 & not LIN a,b,c & c <> c9 holds
o in Clet P,
C be
Subset of
AP;
for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & 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 & b,c // b9,c9 & not LIN a,b,c & c <> c9 holds
o in Clet o,
a,
b,
c,
a9,
b9,
c9 be
Element of
AP;
( o in A & o in P & 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 & b,c // b9,c9 & not LIN a,b,c & c <> c9 implies o in C )
assume that A55:
o in A
and A56:
o in P
and A57:
o <> a
and A58:
o <> b
and
o <> c
and A59:
a in A
and A60:
a9 in A
and A61:
b in P
and A62:
b9 in P
and A63:
c in C
and A64:
c9 in C
and A65:
A is
being_line
and A66:
P is
being_line
and A67:
C is
being_line
and A68:
A <> P
and A69:
A <> C
and A70:
a,
b // a9,
b9
and A71:
a,
c // a9,
c9
and A72:
b,
c // b9,
c9
and A73:
not
LIN a,
b,
c
and A74:
c <> c9
;
o in C
set K =
Line (
o,
c9);
assume A75:
not
o in C
;
contradiction
then A76:
Line (
o,
c9) is
being_line
by A64, AFF_1:38;
A77:
a9 <> c9
proof
assume A78:
a9 = c9
;
contradiction
then
b,
c // a9,
b9
by A72, AFF_1:13;
then
(
a,
b // b,
c or
a9 = b9 )
by A70, AFF_1:14;
then
(
b,
a // b,
c or
a9 = b9 )
by AFF_1:13;
then
(
LIN b,
a,
c or
a9 = b9 )
by AFF_1:def 1;
hence
contradiction
by A55, A56, A60, A62, A64, A65, A66, A68, A73, A75, A78, AFF_1:15, AFF_1:30;
verum
end;
A79:
A <> Line (
o,
c9)
proof
assume
A = Line (
o,
c9)
;
contradiction
then A80:
c9 in A
by A55, AFF_1:38;
a9,
c9 // a,
c
by A71, AFF_1:13;
then
c in A
by A59, A60, A65, A77, A80, AFF_1:62;
hence
contradiction
by A63, A64, A65, A67, A69, A74, A80, AFF_1:30;
verum
end;
A81:
a <> c
by A73, AFF_1:16;
A82:
o in Line (
o,
c9)
by A64, A75, AFF_1:38;
A83:
c9 in Line (
o,
c9)
by A64, A75, AFF_1:38;
not
a,
c // Line (
o,
c9)
proof
assume
a,
c // Line (
o,
c9)
;
contradiction
then
a9,
c9 // Line (
o,
c9)
by A71, A81, AFF_1:46;
then
c9,
a9 // Line (
o,
c9)
by AFF_1:48;
then
a9 in Line (
o,
c9)
by A76, A83, AFF_1:37;
then A84:
a9 in P
by A55, A56, A60, A65, A76, A82, A79, AFF_1:30;
a9,
b9 // b,
a
by A70, AFF_1:13;
then
(
a9 = b9 or
a in P )
by A61, A62, A66, A84, AFF_1:62;
then
a,
c // b,
c
by A55, A56, A57, A59, A65, A66, A68, A71, A72, A77, AFF_1:14, AFF_1:30;
then
c,
a // c,
b
by AFF_1:13;
then
LIN c,
a,
b
by AFF_1:def 1;
hence
contradiction
by A73, AFF_1:15;
verum
end;
then consider x being
Element of
AP such that A85:
x in Line (
o,
c9)
and A86:
LIN a,
c,
x
by A76, AFF_1:73;
A87:
o <> x
proof
assume
o = x
;
contradiction
then
LIN a,
o,
c
by A86, AFF_1:15;
then A88:
c in A
by A55, A57, A59, A65, AFF_1:39;
then
c9 in A
by A59, A60, A65, A71, A81, AFF_1:62;
hence
contradiction
by A63, A64, A65, A67, A69, A74, A88, AFF_1:30;
verum
end;
A89:
b9 <> c9
proof
assume
b9 = c9
;
contradiction
then
(
a9 = b9 or
a,
c // a,
b )
by A70, A71, AFF_1:14;
then
(
a9 = b9 or
LIN a,
c,
b )
by AFF_1:def 1;
then
b,
c // a,
c
by A71, A72, A73, A77, AFF_1:14, AFF_1:15;
then
c,
b // c,
a
by AFF_1:13;
then
LIN c,
b,
a
by AFF_1:def 1;
hence
contradiction
by A73, AFF_1:15;
verum
end;
A90:
a,
c // a,
x
by A86, AFF_1:def 1;
then
a,
x // a9,
c9
by A71, A81, AFF_1:14;
then
b,
x // b9,
c9
by A54, A55, A56, A57, A58, A59, A60, A61, A62, A65, A66, A68, A70, A76, A82, A83, A79, A85, A87, Def4;
then A91:
b,
x // b,
c
by A72, A89, AFF_1:14;
A92:
not
LIN a,
b,
x
proof
assume
LIN a,
b,
x
;
contradiction
then
a,
b // a,
x
by AFF_1:def 1;
then
(
a,
b // a,
c or
a = x )
by A90, AFF_1:14;
hence
contradiction
by A55, A57, A59, A65, A73, A76, A82, A79, A85, AFF_1:30, AFF_1:def 1;
verum
end;
LIN a,
x,
c
by A86, AFF_1:15;
then
c in Line (
o,
c9)
by A85, A92, A91, AFF_1:23;
hence
contradiction
by A63, A64, A67, A74, A75, A76, A82, A83, AFF_1:30;
verum
end;
end;
assume A2:
AP is satisfying_DES_1
; AP is Desarguesian
let A be Subset of AP; AFF_2:def 4 for P, C being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP 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 P, C be Subset of AP; for o, a, b, c, a9, b9, c9 being Element of AP 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 AP; ( 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,c9
assume A22:
not b,c // b9,c9
; contradiction
A23:
a9 <> b9
proof
A24:
a9,
c9 // c,
a
by A21, AFF_1:13;
assume A25:
a9 = b9
;
contradiction
then
a9 in C
by A3, A4, A5, A10, A12, A15, A16, A18, AFF_1:30;
then
(
a in C or
a9 = c9 )
by A13, A14, A17, A24, AFF_1:62;
hence
contradiction
by A3, A5, A6, A9, A15, A17, A19, A22, A25, AFF_1:12, AFF_1:30;
verum
end;
A26:
a9 <> c9
proof
assume
a9 = c9
;
contradiction
then A27:
a9 in P
by A3, A4, A5, A10, A14, A15, A17, A19, AFF_1:30;
a9,
b9 // b,
a
by A20, AFF_1:13;
then
a in P
by A11, A12, A16, A23, A27, AFF_1:62;
hence
contradiction
by A3, A4, A6, A9, A15, A16, A18, AFF_1:30;
verum
end;
A28:
o <> c9
proof
assume A29:
o = c9
;
contradiction
a9,
c9 // a,
c
by A21, AFF_1:13;
then
c in A
by A3, A9, A10, A15, A26, A29, AFF_1:62;
hence
contradiction
by A3, A5, A8, A13, A15, A17, A19, AFF_1:30;
verum
end;
set M = Line (a,c);
set N = Line (b9,c9);
A30:
a <> c
by A3, A5, A6, A9, A13, A15, A17, A19, AFF_1:30;
then A31:
c in Line (a,c)
by AFF_1:38;
A32:
a <> b
by A3, A4, A6, A9, A11, A15, A16, A18, AFF_1:30;
A33:
not LIN a9,b9,c9
proof
assume A34:
LIN a9,
b9,
c9
;
contradiction
then
a9,
b9 // a9,
c9
by AFF_1:def 1;
then
a9,
b9 // a,
c
by A21, A26, AFF_1:14;
then
a,
b // a,
c
by A20, A23, AFF_1:14;
then
LIN a,
b,
c
by AFF_1:def 1;
then
LIN b,
c,
a
by AFF_1:15;
then
b,
c // b,
a
by AFF_1:def 1;
then
b,
c // a,
b
by AFF_1:13;
then A35:
b,
c // a9,
b9
by A20, A32, AFF_1:14;
LIN b9,
c9,
a9
by A34, AFF_1:15;
then
b9,
c9 // b9,
a9
by AFF_1:def 1;
then
b9,
c9 // a9,
b9
by AFF_1:13;
hence
contradiction
by A22, A23, A35, AFF_1:14;
verum
end;
A36:
b9 <> c9
by A22, AFF_1:12;
then A37:
( b9 in Line (b9,c9) & c9 in Line (b9,c9) )
by AFF_1:38;
Line (b9,c9) is being_line
by A36, AFF_1:38;
then consider D being Subset of AP such that
A38:
b in D
and
A39:
Line (b9,c9) // D
by AFF_1:63;
A40:
a in Line (a,c)
by A30, AFF_1:38;
A41:
not Line (a,c) // D
proof
assume
Line (
a,
c)
// D
;
contradiction
then
Line (
a,
c)
// Line (
b9,
c9)
by A39, AFF_1:58;
then
a,
c // b9,
c9
by A40, A31, A37, AFF_1:53;
then
a9,
c9 // b9,
c9
by A21, A30, AFF_1:14;
then
c9,
a9 // c9,
b9
by AFF_1:13;
then
LIN c9,
a9,
b9
by AFF_1:def 1;
hence
contradiction
by A33, AFF_1:15;
verum
end;
A42:
Line (a,c) is being_line
by A30, AFF_1:38;
D is being_line
by A39, AFF_1:50;
then consider x being Element of AP such that
A43:
x in Line (a,c)
and
A44:
x in D
by A42, A41, AFF_1:72;
LIN a,c,x
by A42, A40, A31, A43, AFF_1:33;
then
a,c // a,x
by AFF_1:def 1;
then A45:
a,x // a9,c9
by A21, A30, AFF_1:14;
set T = Line (c9,x);
A46:
a <> a9
proof
assume A47:
a = a9
;
contradiction
then
LIN a,
c,
c9
by A21, AFF_1:def 1;
then
LIN c,
c9,
a
by AFF_1:15;
then A48:
(
c = c9 or
a in C )
by A13, A14, A17, AFF_1:39;
LIN a,
b,
b9
by A20, A47, AFF_1:def 1;
then
LIN b,
b9,
a
by AFF_1:15;
then
(
b = b9 or
a in P )
by A11, A12, A16, AFF_1:39;
hence
contradiction
by A3, A4, A5, A6, A9, A15, A16, A17, A18, A19, A22, A48, AFF_1:11, AFF_1:30;
verum
end;
A49:
x <> c9
proof
assume
x = c9
;
contradiction
then
c9,
a // c9,
a9
by A45, AFF_1:13;
then
LIN c9,
a,
a9
by AFF_1:def 1;
then
LIN a,
a9,
c9
by AFF_1:15;
then
c9 in A
by A9, A10, A15, A46, AFF_1:39;
hence
contradiction
by A3, A5, A14, A15, A17, A19, A28, AFF_1:30;
verum
end;
then A50:
( Line (c9,x) is being_line & c9 in Line (c9,x) )
by AFF_1:38;
A51:
b,x // b9,c9
by A37, A38, A39, A44, AFF_1:53;
A52:
x in Line (c9,x)
by A49, AFF_1:38;
A53:
a <> x
proof
assume
a = x
;
contradiction
then
a,
b // b9,
c9
by A37, A38, A39, A44, AFF_1:53;
then
a9,
b9 // b9,
c9
by A20, A32, AFF_1:14;
then
b9,
a9 // b9,
c9
by AFF_1:13;
then
LIN b9,
a9,
c9
by AFF_1:def 1;
hence
contradiction
by A33, AFF_1:15;
verum
end;
not LIN a,b,x
proof
assume
LIN a,
b,
x
;
contradiction
then
a,
b // a,
x
by AFF_1:def 1;
then
a,
b // a9,
c9
by A45, A53, AFF_1:14;
then
a9,
b9 // a9,
c9
by A20, A32, AFF_1:14;
hence
contradiction
by A33, AFF_1:def 1;
verum
end;
then
o in Line (c9,x)
by A2, A3, A4, A6, A7, A9, A10, A11, A12, A15, A16, A18, A20, A45, A51, A49, A50, A52, Def5;
then
x in C
by A5, A14, A17, A28, A50, A52, AFF_1:30;
then
C = Line (a,c)
by A13, A17, A22, A42, A31, A43, A51, AFF_1:30;
hence
contradiction
by A3, A5, A6, A9, A15, A17, A19, A40, AFF_1:30; verum