let SAS be AffinPlane; ( SAS is Pappian implies for a1, a2, a3, b1, b2, b3 being Element of SAS st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds
a3,b1 // a1,b3 )
assume A1:
SAS is Pappian
; for a1, a2, a3, b1, b2, b3 being Element of SAS st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds
a3,b1 // a1,b3
let a1, a2, a3, b1, b2, b3 be Element of SAS; ( a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 implies a3,b1 // a1,b3 )
assume that
A2:
a1,a2 // a1,a3
and
A3:
b1,b2 // b1,b3
and
A4:
a1,b2 // a2,b1
and
A5:
a2,b3 // a3,b2
; a3,b1 // a1,b3
LIN a1,a2,a3
by A2, AFF_1:def 1;
then consider M being Subset of SAS such that
A6:
M is being_line
and
A7:
a1 in M
and
A8:
a2 in M
and
A9:
a3 in M
by AFF_1:21;
LIN b1,b2,b3
by A3, AFF_1:def 1;
then consider N being Subset of SAS such that
A10:
N is being_line
and
A11:
b1 in N
and
A12:
b2 in N
and
A13:
b3 in N
by AFF_1:21;
A14:
now ( M <> N & not M // N implies a3,b1 // a1,b3 )assume that A15:
M <> N
and A16:
not
M // N
;
a3,b1 // a1,b3consider o being
Element of
SAS such that A17:
o in M
and A18:
o in N
by A6, A10, A16, AFF_1:58;
A19:
now ( o <> a1 & b1 <> o & o = b3 implies a3,b1 // a1,b3 )assume that A20:
o <> a1
and A21:
b1 <> o
and A22:
o = b3
;
a3,b1 // a1,b3A23:
now ( a2 <> o implies a3,b1 // a1,b3 )assume
a2 <> o
;
a3,b1 // a1,b3then
b2 in M
by A5, A6, A8, A9, A17, A22, AFF_1:48;
then
b2 = o
by A6, A10, A12, A15, A17, A18, AFF_1:18;
then
b1 in M
by A4, A6, A7, A8, A17, A20, AFF_1:48;
hence
a3,
b1 // a1,
b3
by A6, A7, A9, A17, A22, AFF_1:51;
verum end; now ( a2 = o implies a3,b1 // a1,b3 )assume
a2 = o
;
a3,b1 // a1,b3then
o,
b1 // b2,
a1
by A4, AFF_1:4;
then
a1 in N
by A10, A11, A12, A13, A21, A22, AFF_1:48;
hence
a3,
b1 // a1,
b3
by A6, A7, A10, A15, A17, A18, A20, AFF_1:18;
verum end; hence
a3,
b1 // a1,
b3
by A23;
verum end; A24:
now ( o <> a1 & b1 = o implies a3,b1 // a1,b3 )assume that
o <> a1
and A25:
b1 = o
;
a3,b1 // a1,b3A26:
o,
a2 // a1,
b2
by A4, A25, AFF_1:4;
A27:
now ( a2 <> o implies a3,b1 // a1,b3 )assume
a2 <> o
;
a3,b1 // a1,b3then
b2 in M
by A6, A7, A8, A17, A26, AFF_1:48;
then
b2 = o
by A6, A10, A12, A15, A17, A18, AFF_1:18;
then A28:
o,
a3 // a2,
b3
by A5, AFF_1:4;
now ( o <> a3 implies a3,b1 // a1,b3 )assume
o <> a3
;
a3,b1 // a1,b3then
b3 in M
by A6, A8, A9, A17, A28, AFF_1:48;
hence
a3,
b1 // a1,
b3
by A6, A7, A9, A17, A25, AFF_1:51;
verum end; hence
a3,
b1 // a1,
b3
by A25, AFF_1:3;
verum end; now ( a2 = o implies a3,b1 // a1,b3 )assume A29:
a2 = o
;
a3,b1 // a1,b3now ( b3 <> o implies a3,b1 // a1,b3 )assume A30:
b3 <> o
;
a3,b1 // a1,b3
o,
b3 // b2,
a3
by A5, A29, AFF_1:4;
then
a3 in N
by A10, A12, A13, A18, A30, AFF_1:48;
then
b1 = a3
by A6, A9, A10, A15, A17, A18, A25, AFF_1:18;
hence
a3,
b1 // a1,
b3
by AFF_1:3;
verum end; hence
a3,
b1 // a1,
b3
by A6, A7, A9, A17, A25, AFF_1:51;
verum end; hence
a3,
b1 // a1,
b3
by A27;
verum end; A31:
now ( o = a1 implies a3,b1 // a1,b3 )assume A32:
o = a1
;
a3,b1 // a1,b3then A33:
o,
b2 // b1,
a2
by A4, AFF_1:4;
A34:
now ( b2 <> o implies a3,b1 // a1,b3 )assume
b2 <> o
;
a3,b1 // a1,b3then
a2 in N
by A10, A11, A12, A18, A33, AFF_1:48;
then
a2 = o
by A6, A8, A10, A15, A17, A18, AFF_1:18;
then A35:
o,
b3 // b2,
a3
by A5, AFF_1:4;
now ( o <> b3 implies a3,b1 // a1,b3 )assume
o <> b3
;
a3,b1 // a1,b3then
a3 in N
by A10, A12, A13, A18, A35, AFF_1:48;
hence
a3,
b1 // a1,
b3
by A10, A11, A13, A18, A32, AFF_1:51;
verum end; hence
a3,
b1 // a1,
b3
by A32, AFF_1:3;
verum end; now ( b2 = o implies a3,b1 // a1,b3 )assume A36:
b2 = o
;
a3,b1 // a1,b3now ( a3 <> o implies a3,b1 // a1,b3 )assume A37:
a3 <> o
;
a3,b1 // a1,b3
o,
a3 // a2,
b3
by A5, A36, AFF_1:4;
then
b3 in M
by A6, A8, A9, A17, A37, AFF_1:48;
then
a1 = b3
by A6, A10, A13, A15, A17, A18, A32, AFF_1:18;
hence
a3,
b1 // a1,
b3
by AFF_1:3;
verum end; hence
a3,
b1 // a1,
b3
by A10, A11, A13, A18, A32, AFF_1:51;
verum end; hence
a3,
b1 // a1,
b3
by A34;
verum end; A38:
now ( o <> a1 & b1 <> o & o <> b3 & o = a3 implies a3,b1 // a1,b3 )assume that A39:
o <> a1
and A40:
b1 <> o
and
o <> b3
and A41:
o = a3
;
a3,b1 // a1,b3A42:
o,
b2 // b3,
a2
by A5, A41, AFF_1:4;
A43:
now ( b2 <> o implies a3,b1 // a1,b3 )assume
b2 <> o
;
a3,b1 // a1,b3then
a2 in N
by A10, A12, A13, A18, A42, AFF_1:48;
then
a2 = o
by A6, A8, A10, A15, A17, A18, AFF_1:18;
then
o,
b1 // b2,
a1
by A4, AFF_1:4;
then
a1 in N
by A10, A11, A12, A18, A40, AFF_1:48;
hence
a3,
b1 // a1,
b3
by A10, A11, A13, A18, A41, AFF_1:51;
verum end; now ( b2 = o implies a3,b1 // a1,b3 )assume
b2 = o
;
a3,b1 // a1,b3then
b1 in M
by A4, A6, A7, A8, A9, A39, A41, AFF_1:48;
hence
a3,
b1 // a1,
b3
by A6, A10, A11, A15, A17, A18, A40, AFF_1:18;
verum end; hence
a3,
b1 // a1,
b3
by A43;
verum end; now ( o <> a1 & o <> b1 & o <> b3 & o <> a3 implies a3,b1 // a1,b3 )assume that A44:
(
o <> a1 &
o <> b1 )
and A45:
o <> b3
and A46:
o <> a3
;
a3,b1 // a1,b3A47:
o <> b2
proof
assume
o = b2
;
contradiction
then
o,
a3 // a2,
b3
by A5, AFF_1:4;
then
b3 in M
by A6, A8, A9, A17, A46, AFF_1:48;
hence
contradiction
by A6, A10, A13, A15, A17, A18, A45, AFF_1:18;
verum
end;
o <> a2
proof
assume
o = a2
;
contradiction
then
o,
b3 // b2,
a3
by A5, AFF_1:4;
then
a3 in N
by A10, A12, A13, A18, A45, AFF_1:48;
hence
contradiction
by A6, A9, A10, A15, A17, A18, A46, AFF_1:18;
verum
end; then
a1,
b3 // a3,
b1
by A1, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A15, A17, A18, A44, A45, A46, A47, AFF_2:def 2;
hence
a3,
b1 // a1,
b3
by AFF_1:4;
verum end; hence
a3,
b1 // a1,
b3
by A31, A24, A19, A38;
verum end;
A48:
SAS is satisfying_pap
by A1, AFF_2:9;
now ( M <> N & M // N implies a3,b1 // a1,b3 )assume
(
M <> N &
M // N )
;
a3,b1 // a1,b3then
a1,
b3 // a3,
b1
by A48, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, AFF_2:def 13;
hence
a3,
b1 // a1,
b3
by AFF_1:4;
verum end;
hence
a3,b1 // a1,b3
by A6, A7, A9, A11, A13, A14, AFF_1:51; verum