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