let AP be AffinPlane; ( AP is Pappian implies AP is satisfying_pap )
assume A1:
AP is Pappian
; 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
A14:
b <> a9
by A5, A7, A8, A9, AFF_1:45;
set K = Line (a,c9);
set C = Line (c,b9);
A15:
c <> b9
by A6, A7, A8, A10, AFF_1:45;
then A16:
Line (c,b9) is being_line
by AFF_1:24;
assume A17:
not a,c9 // c,a9
; contradiction
A18:
now not a = bassume A19:
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, A17, A19, AFF_1:45;
verum end;
A20:
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, A18, AFF_1:25;
hence
contradiction
by A7, A8, A9, AFF_1:45;
verum end;
A21:
now not b = cassume A22:
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, A17, A22, AFF_1:45;
verum end;
A23:
now not b9 = c9assume
b9 = c9
;
contradictionthen
b9,
b // b9,
c
by A13, AFF_1:4;
then
LIN b9,
b,
c
by AFF_1:def 1;
then
LIN b,
c,
b9
by AFF_1:6;
then
b9 in M
by A2, A5, A6, A21, AFF_1:25;
hence
contradiction
by A7, A8, A10, AFF_1:45;
verum end;
A24:
a <> c9
by A4, A7, A8, A11, AFF_1:45;
then A25:
a in Line (a,c9)
by AFF_1:24;
Line (a,c9) is being_line
by A24, AFF_1:24;
then consider T being Subset of AP such that
A26:
a9 in T
and
A27:
Line (a,c9) // T
by AFF_1:49;
A28:
T is being_line
by A27, AFF_1:36;
A29:
c9 in Line (a,c9)
by A24, AFF_1:24;
A30:
( c in Line (c,b9) & b9 in Line (c,b9) )
by A15, AFF_1:24;
not Line (c,b9) // T
proof
assume
Line (
c,
b9)
// T
;
contradiction
then
Line (
c,
b9)
// Line (
a,
c9)
by A27, AFF_1:44;
then
c,
b9 // a,
c9
by A25, A29, A30, AFF_1:39;
then
b,
c9 // a,
c9
by A13, A15, AFF_1:5;
then
c9,
b // c9,
a
by AFF_1:4;
then
LIN c9,
b,
a
by AFF_1:def 1;
then
LIN a,
b,
c9
by AFF_1:6;
then
c9 in M
by A2, A4, A5, A18, AFF_1:25;
hence
contradiction
by A7, A8, A11, AFF_1:45;
verum
end;
then consider x being Element of AP such that
A31:
x in Line (c,b9)
and
A32:
x in T
by A16, A28, AFF_1:58;
set D = Line (x,b);
A33:
x <> b
proof
assume
x = b
;
contradiction
then
LIN b,
c,
b9
by A16, A30, A31, AFF_1:21;
then
b9 in M
by A2, A5, A6, A21, AFF_1:25;
hence
contradiction
by A7, A8, A10, AFF_1:45;
verum
end;
then A34:
b in Line (x,b)
by AFF_1:24;
then A35:
Line (x,b) <> N
by A5, A7, A8, AFF_1:45;
A36:
Line (x,b) is being_line
by A33, AFF_1:24;
A37:
x in Line (x,b)
by A33, AFF_1:24;
not Line (x,b) // N
proof
assume
Line (
x,
b)
// N
;
contradiction
then
Line (
x,
b)
// M
by A7, AFF_1:44;
then
x in M
by A5, A37, A34, AFF_1:45;
then
(
c in T or
b9 in M )
by A2, A6, A16, A30, A31, A32, AFF_1:18;
hence
contradiction
by A7, A8, A10, A17, A25, A29, A26, A27, AFF_1:39, AFF_1:45;
verum
end;
then consider o being Element of AP such that
A38:
o in Line (x,b)
and
A39:
o in N
by A3, A36, AFF_1:58;
LIN b9,c,x
by A16, A30, A31, AFF_1:21;
then A40:
b9,c // b9,x
by AFF_1:def 1;
A41:
a9 <> x
proof
assume
a9 = x
;
contradiction
then
b9,
a9 // b9,
c
by A40, AFF_1:4;
then
LIN b9,
a9,
c
by AFF_1:def 1;
then
c in N
by A3, A9, A10, A20, AFF_1:25;
hence
contradiction
by A6, A7, A8, AFF_1:45;
verum
end;
A42:
now not o = xassume
o = x
;
contradictionthen
N = T
by A3, A9, A26, A28, A32, A39, A41, AFF_1:18;
then
N = Line (
a,
c9)
by A11, A29, A27, AFF_1:45;
hence
contradiction
by A4, A7, A8, A25, AFF_1:45;
verum end;
A43:
a,c9 // x,a9
by A25, A29, A26, A27, A32, AFF_1:39;
A44:
now not o = a9assume
o = a9
;
contradictionthen
LIN a9,
b,
x
by A36, A37, A34, A38, AFF_1:21;
then
a9,
b // a9,
x
by AFF_1:def 1;
then
b,
a9 // x,
a9
by AFF_1:4;
then
a,
b9 // x,
a9
by A12, A14, AFF_1:5;
then
a,
b9 // a,
c9
by A43, A41, AFF_1:5;
then
LIN a,
b9,
c9
by AFF_1:def 1;
then
LIN b9,
c9,
a
by AFF_1:6;
then
a in N
by A3, A10, A11, A23, AFF_1:25;
hence
contradiction
by A4, A7, A8, AFF_1:45;
verum end;
c,b9 // x,b9
by A40, AFF_1:4;
then A45:
b,c9 // x,b9
by A13, A15, AFF_1:5;
A46:
a <> b9
by A4, A7, A8, A10, AFF_1:45;
not a,b9 // Line (x,b)
proof
assume
a,
b9 // Line (
x,
b)
;
contradiction
then
b,
a9 // Line (
x,
b)
by A12, A46, AFF_1:32;
then
a9 in Line (
x,
b)
by A36, A34, AFF_1:23;
then
b in T
by A26, A28, A32, A36, A37, A34, A41, AFF_1:18;
then
b,
a9 // a,
c9
by A25, A29, A26, A27, AFF_1:39;
then
a,
b9 // a,
c9
by A12, A14, AFF_1:5;
then
LIN a,
b9,
c9
by AFF_1:def 1;
then
LIN b9,
c9,
a
by AFF_1:6;
then
a in N
by A3, A10, A11, A23, AFF_1:25;
hence
contradiction
by A4, A7, A8, AFF_1:45;
verum
end;
then consider y being Element of AP such that
A47:
y in Line (x,b)
and
A48:
LIN a,b9,y
by A36, AFF_1:59;
A49:
LIN a,y,a
by AFF_1:7;
A50:
b9 <> x
proof
assume
b9 = x
;
contradiction
then
a,
c9 // a9,
b9
by A25, A29, A26, A27, A32, AFF_1:39;
then
a,
c9 // N
by A3, A9, A10, A20, AFF_1:27;
then
c9,
a // N
by AFF_1:34;
then
a in N
by A3, A11, AFF_1:23;
hence
contradiction
by A4, A7, A8, AFF_1:45;
verum
end;
A51:
now not o = b9assume
o = b9
;
contradictionthen
LIN b9,
x,
b
by A36, A37, A34, A38, AFF_1:21;
then
b9,
x // b9,
b
by AFF_1:def 1;
then
x,
b9 // b,
b9
by AFF_1:4;
then
b,
c9 // b,
b9
by A45, A50, AFF_1:5;
then
LIN b,
c9,
b9
by AFF_1:def 1;
then
LIN b9,
c9,
b
by AFF_1:6;
then
b in N
by A3, A10, A11, A23, AFF_1:25;
hence
contradiction
by A5, A7, A8, AFF_1:45;
verum end;
A52:
now not o = yassume
o = y
;
contradictionthen
LIN b9,
o,
a
by A48, AFF_1:6;
then
a in N
by A3, A10, A39, A51, AFF_1:25;
hence
contradiction
by A4, A7, A8, AFF_1:45;
verum end;
A53:
b <> c9
by A5, A7, A8, A11, AFF_1:45;
A54:
now not o = c9assume
o = c9
;
contradictionthen
Line (
x,
b)
// Line (
c,
b9)
by A13, A15, A53, A16, A30, A36, A34, A38, AFF_1:38;
then
b in Line (
c,
b9)
by A31, A37, A34, AFF_1:45;
then
LIN c,
b,
b9
by A16, A30, AFF_1:21;
then
b9 in M
by A2, A5, A6, A21, AFF_1:25;
hence
contradiction
by A7, A8, A10, AFF_1:45;
verum end;
LIN b9,a,y
by A48, AFF_1:6;
then
b9,a // b9,y
by AFF_1:def 1;
then
a,b9 // y,b9
by AFF_1:4;
then A55:
y,b9 // b,a9
by A12, A46, AFF_1:5;
o <> b
by A5, A7, A8, A39, AFF_1:45;
then
y,c9 // x,a9
by A1, A3, A9, A10, A11, A36, A37, A34, A38, A39, A45, A47, A55, A35, A51, A44, A54, A42, A52;
then
y,c9 // a,c9
by A43, A41, AFF_1:5;
then
c9,y // c9,a
by AFF_1:4;
then
LIN c9,y,a
by AFF_1:def 1;
then A56:
LIN a,y,c9
by AFF_1:6;
LIN a,y,b9
by A48, AFF_1:6;
then
( a in Line (x,b) or a in N )
by A3, A10, A11, A23, A47, A56, A49, AFF_1:8, AFF_1:25;
then
Line (x,b) // N
by A2, A4, A5, A7, A8, A18, A36, A34, AFF_1:18, AFF_1:45;
hence
contradiction
by A38, A39, A35, AFF_1:45; verum