let AP be AffinPlane; ( AP is Pappian iff AP is satisfying_PAP_1 )
hereby ( AP is satisfying_PAP_1 implies AP is Pappian )
assume A1:
AP is
Pappian
;
AP is satisfying_PAP_1 thus
AP is
satisfying_PAP_1
verumproof
let M be
Subset of
AP;
AFF_2:def 3 for N being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & b <> c holds
a9 in Nlet N be
Subset of
AP;
for o, a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & b <> c holds
a9 in Nlet o,
a,
b,
c,
a9,
b9,
c9 be
Element of
AP;
( M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & b <> c implies a9 in N )
assume that A2:
M is
being_line
and A3:
N is
being_line
and A4:
M <> N
and A5:
o in M
and A6:
o in N
and A7:
o <> a
and
o <> a9
and A8:
o <> b
and A9:
o <> b9
and A10:
o <> c
and A11:
o <> c9
and A12:
a in M
and A13:
b in M
and A14:
c in M
and A15:
b9 in N
and A16:
c9 in N
and A17:
a,
b9 // b,
a9
and A18:
b,
c9 // c,
b9
and A19:
a,
c9 // c,
a9
and A20:
b <> c
;
a9 in N
A21:
a <> c9
by A2, A3, A4, A5, A6, A7, A12, A16, AFF_1:18;
A22:
b <> a9
proof
assume
b = a9
;
contradiction
then
c,
b // a,
c9
by A19, AFF_1:4;
then
c9 in M
by A2, A12, A13, A14, A20, AFF_1:48;
hence
contradiction
by A2, A3, A4, A5, A6, A11, A16, AFF_1:18;
verum
end;
not
b,
a9 // N
proof
assume A23:
b,
a9 // N
;
contradiction
b,
a9 // a,
b9
by A17, AFF_1:4;
then
a,
b9 // N
by A22, A23, AFF_1:32;
then
b9,
a // N
by AFF_1:34;
then
a in N
by A3, A15, AFF_1:23;
hence
contradiction
by A2, A3, A4, A5, A6, A7, A12, AFF_1:18;
verum
end;
then consider x being
Element of
AP such that A24:
x in N
and A25:
LIN b,
a9,
x
by A3, AFF_1:59;
A26:
b,
a9 // b,
x
by A25, AFF_1:def 1;
A27:
o <> x
proof
assume
o = x
;
contradiction
then
b,
o // a,
b9
by A17, A22, A26, AFF_1:5;
then
b9 in M
by A2, A5, A8, A12, A13, AFF_1:48;
hence
contradiction
by A2, A3, A4, A5, A6, A9, A15, AFF_1:18;
verum
end;
a,
b9 // b,
x
by A17, A22, A26, AFF_1:5;
then
a,
c9 // c,
x
by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A18, A24, A27;
then
c,
a9 // c,
x
by A19, A21, AFF_1:5;
then
LIN c,
a9,
x
by AFF_1:def 1;
then A28:
LIN a9,
x,
c
by AFF_1:6;
A29:
LIN a9,
x,
x
by AFF_1:7;
assume A30:
not
a9 in N
;
contradiction
LIN a9,
x,
b
by A25, AFF_1:6;
then
x in M
by A2, A13, A14, A20, A30, A24, A28, A29, AFF_1:8, AFF_1:25;
hence
contradiction
by A2, A3, A4, A5, A6, A24, A27, AFF_1:18;
verum
end;
end;
assume A31:
AP is satisfying_PAP_1
; AP is Pappian
let M be Subset of AP; AFF_2:def 2 for N being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & 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 o, a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9
let o, a, b, c, a9, b9, c9 be Element of AP; ( M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 implies a,c9 // c,a9 )
assume that
A32:
M is being_line
and
A33:
N is being_line
and
A34:
( M <> N & o in M & o in N )
and
A35:
o <> a
and
A36:
o <> a9
and
A37:
o <> b
and
A38:
o <> b9
and
A39:
( o <> c & o <> c9 )
and
A40:
a in M
and
A41:
b in M
and
A42:
c in M
and
A43:
a9 in N
and
A44:
b9 in N
and
A45:
c9 in N
and
A46:
a,b9 // b,a9
and
A47:
b,c9 // c,b9
; a,c9 // c,a9
set A = Line (a,c9);
set P = Line (b,a9);
A48:
b <> a9
by A32, A33, A34, A36, A41, A43, AFF_1:18;
then A49:
b in Line (b,a9)
by AFF_1:24;
assume A50:
not a,c9 // c,a9
; contradiction
then A51:
a <> c9
by AFF_1:3;
then A52:
( a in Line (a,c9) & c9 in Line (a,c9) )
by AFF_1:24;
A53:
a9 in Line (b,a9)
by A48, AFF_1:24;
Line (a,c9) is being_line
by A51, AFF_1:24;
then consider K being Subset of AP such that
A54:
c in K
and
A55:
Line (a,c9) // K
by AFF_1:49;
A56:
b <> c
proof
assume A57:
b = c
;
contradiction
then
LIN b,
c9,
b9
by A47, AFF_1:def 1;
then
LIN b9,
c9,
b
by AFF_1:6;
then
(
b9 = c9 or
b in N )
by A33, A44, A45, AFF_1:25;
hence
contradiction
by A32, A33, A34, A37, A41, A46, A50, A57, AFF_1:18;
verum
end;
A58:
b9 <> c9
proof
assume
b9 = c9
;
contradiction
then
b9,
b // b9,
c
by A47, 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 A32, A41, A42, A56, AFF_1:25;
hence
contradiction
by A32, A33, A34, A38, A44, AFF_1:18;
verum
end;
A59:
not Line (b,a9) // K
proof
assume
Line (
b,
a9)
// K
;
contradiction
then
Line (
b,
a9)
// Line (
a,
c9)
by A55, AFF_1:44;
then
b,
a9 // a,
c9
by A52, A49, A53, AFF_1:39;
then
a,
b9 // a,
c9
by A46, A48, 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 A33, A44, A45, A58, AFF_1:25;
hence
contradiction
by A32, A33, A34, A35, A40, AFF_1:18;
verum
end;
A60:
Line (b,a9) is being_line
by A48, AFF_1:24;
K is being_line
by A55, AFF_1:36;
then consider x being Element of AP such that
A61:
x in Line (b,a9)
and
A62:
x in K
by A60, A59, AFF_1:58;
A63:
a,c9 // c,x
by A52, A54, A55, A62, AFF_1:39;
LIN b,x,a9
by A60, A49, A53, A61, AFF_1:21;
then
b,x // b,a9
by AFF_1:def 1;
then
a,b9 // b,x
by A46, A48, AFF_1:5;
then
x in N
by A31, A32, A33, A34, A35, A37, A38, A39, A40, A41, A42, A44, A45, A47, A56, A63;
then
N = Line (b,a9)
by A33, A43, A50, A60, A53, A61, A63, AFF_1:18;
hence
contradiction
by A32, A33, A34, A37, A41, A49, AFF_1:18; verum