let AP be AffinPlane; ( AP is satisfying_DES1_3 implies AP is satisfying_DES2_1 )
assume A1:
AP is satisfying_DES1_3
; AP is satisfying_DES2_1
let A be Subset of AP; AFF_3:def 6 for P, C being Subset of AP
for 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 & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds
a,c // a9,c9
let P, C be Subset of AP; for 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 & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds
a,c // a9,c9
let a, a9, b, b9, c, c9, p, q be Element of AP; ( A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q implies a,c // a9,c9 )
assume that
A2:
A is being_line
and
A3:
P is being_line
and
A4:
C is being_line
and
A5:
A <> P
and
A6:
A <> C
and
A7:
P <> C
and
A8:
a in A
and
A9:
a9 in A
and
A10:
b in P
and
A11:
b9 in P
and
A12:
c in C
and
A13:
c9 in C
and
A14:
A // P
and
A15:
A // C
and
A16:
not LIN b,a,c
and
A17:
not LIN b9,a9,c9
and
A18:
p <> q
and
A19:
LIN b,a,p
and
A20:
LIN b9,a9,p
and
A21:
LIN b,c,q
and
A22:
LIN b9,c9,q
and
A23:
a,c // p,q
; a,c // a9,c9
A24:
P // C
by A14, A15, AFF_1:44;
set K = Line (p,q);
set M = Line (a,c);
set N = Line (a9,c9);
A25:
a <> c
by A16, AFF_1:7;
then A26:
a in Line (a,c)
by AFF_1:24;
A27:
( c,c9 // a,a9 & LIN q,c,b )
by A8, A9, A12, A13, A15, A21, AFF_1:6, AFF_1:39;
A28:
LIN p,a9,b9
by A20, AFF_1:6;
C // P
by A14, A15, AFF_1:44;
then A29:
c,c9 // b,b9
by A10, A11, A12, A13, AFF_1:39;
A30:
( LIN q,c9,b9 & LIN p,a,b )
by A19, A22, AFF_1:6;
A31:
c in Line (a,c)
by A25, AFF_1:24;
assume A32:
not a,c // a9,c9
; contradiction
A33:
c <> q
proof
assume A34:
c = q
;
contradiction
then
c,
a // c,
p
by A23, AFF_1:4;
then
LIN c,
a,
p
by AFF_1:def 1;
then A35:
LIN p,
a,
c
by AFF_1:6;
(
LIN p,
a,
b &
LIN p,
a,
a )
by A19, AFF_1:6, AFF_1:7;
then
p = a
by A16, A35, AFF_1:8;
then
LIN a,
a9,
b9
by A20, AFF_1:6;
then A36:
(
a = a9 or
b9 in A )
by A2, A8, A9, AFF_1:25;
LIN c,
c9,
b9
by A22, A34, AFF_1:6;
then
(
c = c9 or
b9 in C )
by A4, A12, A13, AFF_1:25;
hence
contradiction
by A5, A7, A11, A14, A32, A24, A36, AFF_1:2, AFF_1:45;
verum
end;
A37:
c <> c9
proof
A38:
now not p = bassume A39:
p = b
;
contradiction
LIN b,
q,
c
by A21, AFF_1:6;
then
b,
q // b,
c
by AFF_1:def 1;
then
(
a,
c // b,
c or
b = q )
by A23, A39, AFF_1:5;
then
c,
a // c,
b
by A18, A39, AFF_1:4;
then
LIN c,
a,
b
by AFF_1:def 1;
hence
contradiction
by A16, AFF_1:6;
verum end;
A40:
(
LIN q,
c,
b &
LIN q,
c,
c )
by A21, AFF_1:6, AFF_1:7;
assume A41:
c = c9
;
contradiction
then
LIN q,
c,
b9
by A22, AFF_1:6;
then
(
b = b9 or
c in P )
by A3, A10, A11, A33, A40, AFF_1:8, AFF_1:25;
then A42:
LIN p,
b,
a9
by A7, A12, A20, A24, AFF_1:6, AFF_1:45;
(
LIN p,
b,
a &
LIN p,
b,
b )
by A19, AFF_1:6, AFF_1:7;
then
(
a = a9 or
b in A )
by A2, A8, A9, A42, A38, AFF_1:8, AFF_1:25;
hence
contradiction
by A5, A10, A14, A32, A41, AFF_1:2, AFF_1:45;
verum
end;
A43:
b <> b9
proof
assume
b = b9
;
contradiction
then A44:
LIN q,
b,
c9
by A22, AFF_1:6;
(
LIN q,
b,
c &
LIN q,
b,
b )
by A21, AFF_1:6, AFF_1:7;
then A45:
(
q = b or
b in C )
by A4, A12, A13, A37, A44, AFF_1:8, AFF_1:25;
b,
a // b,
p
by A19, AFF_1:def 1;
then
a,
b // p,
b
by AFF_1:4;
then
(
a,
c // a,
b or
p = b )
by A7, A10, A23, A24, A45, AFF_1:5, AFF_1:45;
then
LIN a,
c,
b
by A7, A10, A18, A24, A45, AFF_1:45, AFF_1:def 1;
hence
contradiction
by A16, AFF_1:6;
verum
end;
A46:
not LIN q,c,c9
proof
assume A47:
LIN q,
c,
c9
;
contradiction
(
LIN q,
c,
b &
LIN q,
c,
c )
by A21, AFF_1:6, AFF_1:7;
then
b in C
by A4, A12, A13, A33, A37, A47, AFF_1:8, AFF_1:25;
hence
contradiction
by A7, A10, A24, AFF_1:45;
verum
end;
A48:
a9 <> c9
by A17, AFF_1:7;
then A49:
Line (a9,c9) is being_line
by AFF_1:24;
A50:
p <> a
proof
assume
p = a
;
contradiction
then
LIN a,
c,
q
by A23, AFF_1:def 1;
then A51:
LIN c,
q,
a
by AFF_1:6;
(
LIN c,
q,
b &
LIN c,
q,
c )
by A21, AFF_1:6, AFF_1:7;
hence
contradiction
by A16, A33, A51, AFF_1:8;
verum
end;
A52:
not LIN p,a,a9
proof
assume A53:
LIN p,
a,
a9
;
contradiction
(
LIN p,
a,
b &
LIN p,
a,
a )
by A19, AFF_1:6, AFF_1:7;
then
(
a = a9 or
b in A )
by A2, A8, A9, A50, A53, AFF_1:8, AFF_1:25;
then A54:
LIN p,
a,
b9
by A5, A10, A14, A20, AFF_1:6, AFF_1:45;
(
LIN p,
a,
b &
LIN p,
a,
a )
by A19, AFF_1:6, AFF_1:7;
then
a in P
by A3, A10, A11, A43, A50, A54, AFF_1:8, AFF_1:25;
hence
contradiction
by A5, A8, A14, AFF_1:45;
verum
end;
A55:
Line (a,c) is being_line
by A25, AFF_1:24;
A56:
( Line (p,q) is being_line & q in Line (p,q) )
by A18, AFF_1:24;
A57:
now not Line (a,c) = Line (p,q)assume
Line (
a,
c)
= Line (
p,
q)
;
contradictionthen A58:
(
LIN q,
c,
a &
LIN q,
c,
c )
by A56, A26, A31, AFF_1:21;
LIN q,
c,
b
by A21, AFF_1:6;
hence
contradiction
by A16, A33, A58, AFF_1:8;
verum end;
A59:
c9 in Line (a9,c9)
by A48, AFF_1:24;
A60:
a9 in Line (a9,c9)
by A48, AFF_1:24;
then consider x being Element of AP such that
A61:
x in Line (a,c)
and
A62:
x in Line (a9,c9)
by A32, A55, A49, A26, A31, A59, AFF_1:39, AFF_1:58;
A63:
now not x = cassume
x = c
;
contradictionthen
Line (
a9,
c9)
= C
by A4, A12, A13, A37, A49, A59, A62, AFF_1:18;
hence
contradiction
by A6, A9, A15, A60, AFF_1:45;
verum end;
A64:
p in Line (p,q)
by A18, AFF_1:24;
then A65:
Line (a,c) // Line (p,q)
by A18, A23, A25, A55, A56, A26, A31, AFF_1:38;
A66:
now not x = c9assume
x = c9
;
contradictionthen
Line (
a,
c)
= C
by A4, A12, A13, A37, A55, A31, A61, AFF_1:18;
hence
contradiction
by A6, A8, A15, A26, AFF_1:45;
verum end;
Line (a,c) <> Line (a9,c9)
by A32, A55, A26, A31, A60, A59, AFF_1:51;
then
x in Line (p,q)
by A1, A18, A25, A55, A49, A64, A56, A26, A31, A60, A59, A61, A62, A29, A27, A30, A28, A43, A63, A66, A46, A52;
hence
contradiction
by A65, A61, A57, AFF_1:45; verum