let AP be AffinPlane; ( AP is Desarguesian implies AP is satisfying_DES1_2 )
assume A1:
AP is Desarguesian
; AP is satisfying_DES1_2
then A2:
AP is satisfying_DES_1
by AFF_2:2;
let A be Subset of AP; AFF_3:def 3 for P, C being Subset of AP
for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds
o in C
let P, C be Subset of AP; for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds
o in C
let o, a, a9, b, b9, c, c9, p, q be Element of AP; ( A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q implies o in C )
assume that
A3:
A is being_line
and
A4:
P is being_line
and
A5:
C is being_line
and
A6:
P <> A
and
A7:
P <> C
and
A <> C
and
A8:
o in A
and
A9:
( a in A & a9 in A )
and
A10:
o in P
and
A11:
b in P
and
A12:
b9 in P
and
A13:
c in C
and
A14:
c9 in C
and
A15:
o <> a
and
A16:
o <> b
and
o <> c
and
A17:
p <> q
and
A18:
not LIN b,a,c
and
A19:
not LIN b9,a9,c9
and
A20:
c <> c9
and
A21:
LIN b,a,p
and
A22:
LIN b9,a9,p
and
A23:
LIN b,c,q
and
A24:
LIN b9,c9,q
and
A25:
a,c // a9,c9
and
A26:
a,c // p,q
; o in C
A27:
b <> p
by A17, A18, A23, A26, AFF_1:55;
set K = Line (b9,a9);
A28:
p in Line (b9,a9)
by A22, AFF_1:def 2;
a9 <> b9
by A19, AFF_1:7;
then A29:
Line (b9,a9) is being_line
by AFF_1:def 3;
A30:
b <> q
proof
assume A31:
b = q
;
contradiction
( not
LIN b,
c,
a &
c,
a // q,
p )
by A18, A26, AFF_1:4, AFF_1:6;
hence
contradiction
by A17, A21, A31, AFF_1:55;
verum
end;
set M = Line (b9,c9);
A32:
q in Line (b9,c9)
by A24, AFF_1:def 2;
A33:
c9 in Line (b9,c9)
by AFF_1:15;
A34:
a <> c
by A18, AFF_1:7;
A35:
b9 <> p
A37:
b9 <> q
proof
a9,
c9 // p,
q
by A25, A26, A34, AFF_1:5;
then A38:
c9,
a9 // q,
p
by AFF_1:4;
assume A39:
b9 = q
;
contradiction
not
LIN b9,
c9,
a9
by A19, AFF_1:6;
hence
contradiction
by A17, A22, A39, A38, AFF_1:55;
verum
end;
A40:
b <> c
by A18, AFF_1:7;
A41:
a <> b
by A18, AFF_1:7;
A42:
( b9 <> a9 & b9 <> c9 )
by A19, AFF_1:7;
A43:
a9 in Line (b9,a9)
by AFF_1:15;
A44:
b9 in Line (b9,c9)
by AFF_1:15;
A45:
b9 <> c9
by A19, AFF_1:7;
then A46:
Line (b9,c9) is being_line
by AFF_1:def 3;
A47:
b9 in Line (b9,a9)
by AFF_1:15;
then A48:
Line (b9,a9) <> Line (b9,c9)
by A19, A29, A43, A33, AFF_1:21;
now o in CA49:
now ( Line (b9,c9) <> P implies o in C )
p,
q // a9,
c9
by A25, A26, A34, AFF_1:5;
then A50:
c9,
a9 // q,
p
by AFF_1:4;
A51:
b,
a // b,
p
by A21, AFF_1:def 1;
set D =
Line (
b,
c);
A52:
b in Line (
b,
c)
by AFF_1:15;
Line (
b,
c) is
being_line
by A40, AFF_1:def 3;
then consider D9 being
Subset of
AP such that A53:
c9 in D9
and A54:
Line (
b,
c)
// D9
by AFF_1:49;
A55:
D9 is
being_line
by A54, AFF_1:36;
A56:
q in Line (
b,
c)
by A23, AFF_1:def 2;
assume A57:
Line (
b9,
c9)
<> P
;
o in C
not
D9 // P
proof
assume
D9 // P
;
contradiction
then
Line (
b,
c)
// P
by A54, AFF_1:44;
then
q in P
by A11, A52, A56, AFF_1:45;
hence
contradiction
by A4, A12, A46, A44, A32, A37, A57, AFF_1:18;
verum
end; then consider d being
Element of
AP such that A58:
d in D9
and A59:
d in P
by A4, A55, AFF_1:58;
A60:
c in Line (
b,
c)
by AFF_1:15;
A61:
d <> b9
proof
assume
d = b9
;
contradiction
then
Line (
b9,
c9)
= D9
by A45, A46, A44, A33, A53, A55, A58, AFF_1:18;
then A62:
Line (
b,
c)
= Line (
b9,
c9)
by A32, A56, A54, AFF_1:45;
then
LIN c,
c9,
b
by A46, A33, A52, A60, AFF_1:21;
then A63:
b in C
by A5, A13, A14, A20, AFF_1:25;
set N =
Line (
a,
c);
set T =
Line (
b,
a);
A64:
b in Line (
b,
a)
by AFF_1:15;
A65:
c in Line (
a,
c)
by AFF_1:15;
A66:
a in Line (
b,
a)
by AFF_1:15;
A67:
Line (
a,
c) is
being_line
by A34, AFF_1:def 3;
A68:
a in Line (
a,
c)
by AFF_1:15;
A69:
a <> a9
proof
assume
a = a9
;
contradiction
then
LIN a,
c,
c9
by A25, AFF_1:def 1;
then
c9 in Line (
a,
c)
by AFF_1:def 2;
then
Line (
a,
c)
= C
by A5, A13, A14, A20, A67, A65, AFF_1:18;
hence
contradiction
by A13, A18, A63, A67, A68, AFF_1:21;
verum
end;
A70:
(
Line (
b,
a) is
being_line &
p in Line (
b,
a) )
by A21, A41, AFF_1:def 2, AFF_1:def 3;
A71:
b <> b9
proof
A72:
Line (
b9,
a9)
<> Line (
b,
a)
proof
assume
Line (
b9,
a9)
= Line (
b,
a)
;
contradiction
then
Line (
b,
a)
= A
by A3, A9, A29, A43, A66, A69, AFF_1:18;
hence
contradiction
by A3, A4, A6, A8, A10, A11, A16, A64, AFF_1:18;
verum
end;
assume
b = b9
;
contradiction
hence
contradiction
by A29, A47, A28, A35, A64, A70, A72, AFF_1:18;
verum
end;
LIN c,
c9,
b9
by A46, A44, A33, A60, A62, AFF_1:21;
then
b9 in C
by A5, A13, A14, A20, AFF_1:25;
hence
contradiction
by A4, A5, A7, A11, A12, A63, A71, AFF_1:18;
verum
end;
c9,
d // q,
b
by A52, A56, A53, A54, A58, AFF_1:39;
then
d,
a9 // b,
p
by A1, A4, A11, A12, A42, A29, A46, A47, A43, A28, A44, A33, A32, A48, A57, A59, A61, A50;
then A73:
b,
a // d,
a9
by A27, A51, AFF_1:5;
b,
c // d,
c9
by A52, A60, A53, A54, A58, AFF_1:39;
hence
o in C
by A2, A3, A4, A5, A6, A8, A9, A10, A11, A13, A14, A15, A16, A18, A20, A25, A59, A73;
verum end; now ( Line (b9,c9) = P implies o in C )assume A74:
Line (
b9,
c9)
= P
;
o in C
LIN b,
q,
c
by A23, AFF_1:6;
then
c in P
by A11, A46, A32, A30, A74, AFF_1:25;
then
P = Line (
c,
c9)
by A20, A46, A33, A74, AFF_1:57;
hence
o in C
by A5, A10, A13, A14, A20, AFF_1:57;
verum end; hence
o in C
by A49;
verum
hence
o in C
; verum