let AP be AffinPlane; ( AP is translational implies AP is satisfying_pap )
assume A1:
AP is translational
; AP is satisfying_pap
let M be Subset of AP; AFF_2:def 13 for N being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9
let N be Subset of AP; for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9
let a, b, c, a9, b9, c9 be Element of AP; ( M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 implies a,c9 // c,a9 )
assume that
A2:
M is being_line
and
A3:
N is being_line
and
A4:
a in M
and
A5:
b in M
and
A6:
c in M
and
A7:
M // N
and
A8:
M <> N
and
A9:
a9 in N
and
A10:
b9 in N
and
A11:
c9 in N
and
A12:
a,b9 // b,a9
and
A13:
b,c9 // c,b9
; a,c9 // c,a9
set A = Line (a,b9);
set A9 = Line (b,a9);
set P = Line (b,c9);
set P9 = Line (c,b9);
A14:
c <> b9
by A6, A7, A8, A10, AFF_1:45;
then A15:
( c in Line (c,b9) & b9 in Line (c,b9) )
by AFF_1:24;
A16:
b <> c9
by A5, A7, A8, A11, AFF_1:45;
then A17:
( Line (b,c9) is being_line & b in Line (b,c9) )
by AFF_1:24;
A18:
Line (c,b9) is being_line
by A14, AFF_1:24;
then consider C9 being Subset of AP such that
A19:
a in C9
and
A20:
Line (c,b9) // C9
by AFF_1:49;
A21:
C9 is being_line
by A20, AFF_1:36;
assume A22:
not a,c9 // c,a9
; contradiction
A23:
now not a = cassume A24:
a = c
;
contradictionthen
b,
c9 // b,
a9
by A12, A13, A14, AFF_1:5;
then
LIN b,
c9,
a9
by AFF_1:def 1;
then
LIN a9,
c9,
b
by AFF_1:6;
then
(
a9 = c9 or
b in N )
by A3, A9, A11, AFF_1:25;
hence
contradiction
by A5, A7, A8, A22, A24, AFF_1:2, AFF_1:45;
verum end;
A25:
Line (c,b9) <> C9
proof
assume
Line (
c,
b9)
= C9
;
contradiction
then
LIN a,
c,
b9
by A18, A15, A19, AFF_1:21;
then
b9 in M
by A2, A4, A6, A23, AFF_1:25;
hence
contradiction
by A7, A8, A10, AFF_1:45;
verum
end;
A26:
c9 in Line (b,c9)
by A16, AFF_1:24;
then A27:
Line (c,b9) // Line (b,c9)
by A13, A16, A14, A18, A17, A15, AFF_1:38;
A28:
now not b = cassume A29:
b = c
;
contradictionthen
LIN b,
c9,
b9
by A13, AFF_1:def 1;
then
LIN b9,
c9,
b
by AFF_1:6;
then
(
b9 = c9 or
b in N )
by A3, A10, A11, AFF_1:25;
hence
contradiction
by A5, A7, A8, A12, A22, A29, AFF_1:45;
verum end;
A30:
Line (c,b9) <> Line (b,c9)
proof
assume
Line (
c,
b9)
= Line (
b,
c9)
;
contradiction
then
LIN b,
c,
b9
by A17, A15, AFF_1:21;
then
b9 in M
by A2, A5, A6, A28, AFF_1:25;
hence
contradiction
by A7, A8, A10, AFF_1:45;
verum
end;
A31:
a <> b9
by A4, A7, A8, A10, AFF_1:45;
then A32:
Line (a,b9) is being_line
by AFF_1:24;
then consider C being Subset of AP such that
A33:
c in C
and
A34:
Line (a,b9) // C
by AFF_1:49;
A35:
C is being_line
by A34, AFF_1:36;
A36:
a,b // b9,a9
by A4, A5, A7, A9, A10, AFF_1:39;
A37:
b9,c9 // c,b
by A5, A6, A7, A10, A11, AFF_1:39;
A38:
b <> a9
by A5, A7, A8, A9, AFF_1:45;
then A39:
a9 in Line (b,a9)
by AFF_1:24;
A40:
( a in Line (a,b9) & b9 in Line (a,b9) )
by A31, AFF_1:24;
A41:
Line (a,b9) <> C
proof
assume
Line (
a,
b9)
= C
;
contradiction
then
LIN a,
c,
b9
by A32, A40, A33, AFF_1:21;
then
b9 in M
by A2, A4, A6, A23, AFF_1:25;
hence
contradiction
by A7, A8, A10, AFF_1:45;
verum
end;
not C // C9
proof
assume
C // C9
;
contradiction
then
Line (
a,
b9)
// C9
by A34, AFF_1:44;
then
Line (
a,
b9)
// Line (
c,
b9)
by A20, AFF_1:44;
then
b9,
a // b9,
c
by A40, A15, AFF_1:39;
then
LIN b9,
a,
c
by AFF_1:def 1;
then
LIN a,
c,
b9
by AFF_1:6;
then
b9 in M
by A2, A4, A6, A23, AFF_1:25;
hence
contradiction
by A7, A8, A10, AFF_1:45;
verum
end;
then consider s being Element of AP such that
A42:
s in C
and
A43:
s in C9
by A35, A21, AFF_1:58;
A44:
( Line (b,a9) is being_line & b in Line (b,a9) )
by A38, AFF_1:24;
A45:
now not a = bassume A46:
a = b
;
contradictionthen
LIN a,
b9,
a9
by A12, AFF_1:def 1;
then
LIN a9,
b9,
a
by AFF_1:6;
then
(
a9 = b9 or
a in N )
by A3, A9, A10, AFF_1:25;
hence
contradiction
by A4, A7, A8, A13, A22, A46, AFF_1:45;
verum end;
A47:
now not a9 = b9assume
a9 = b9
;
contradictionthen
a9,
a // a9,
b
by A12, AFF_1:4;
then
LIN a9,
a,
b
by AFF_1:def 1;
then
LIN a,
b,
a9
by AFF_1:6;
then
a9 in M
by A2, A4, A5, A45, AFF_1:25;
hence
contradiction
by A7, A8, A9, AFF_1:45;
verum end;
A48:
Line (a,b9) <> Line (b,a9)
proof
assume
Line (
a,
b9)
= Line (
b,
a9)
;
contradiction
then
LIN a9,
b9,
a
by A32, A40, A39, AFF_1:21;
then
a in N
by A3, A9, A10, A47, AFF_1:25;
hence
contradiction
by A4, A7, A8, AFF_1:45;
verum
end;
A49:
b <> s
proof
assume
b = s
;
contradiction
then
a,
b9 // b,
c
by A40, A33, A34, A42, AFF_1:39;
then
b,
a9 // b,
c
by A12, A31, AFF_1:5;
then
LIN b,
a9,
c
by AFF_1:def 1;
then
LIN b,
c,
a9
by AFF_1:6;
then
a9 in M
by A2, A5, A6, A28, AFF_1:25;
hence
contradiction
by A7, A8, A9, AFF_1:45;
verum
end;
A50:
Line (a,b9) // Line (b,a9)
by A12, A31, A38, AFF_1:37;
a,s // b9,c
by A15, A19, A20, A43, AFF_1:39;
then A51:
b,s // a9,c
by A1, A32, A40, A44, A39, A33, A34, A35, A42, A36, A48, A41, A50;
b9,a // c,s
by A40, A33, A34, A42, AFF_1:39;
then
c9,a // b,s
by A1, A18, A17, A26, A15, A19, A20, A21, A43, A37, A30, A25, A27;
then
c9,a // a9,c
by A51, A49, AFF_1:5;
hence
contradiction
by A22, AFF_1:4; verum