let X be AffinPlane; :: thesis: ( X is Pappian iff X is satisfying_major_indirect_Scherungssatz )
A1:
( X is Pappian implies X is satisfying_major_indirect_Scherungssatz )
proof
assume A2:
X is
Pappian
;
:: thesis: X is satisfying_major_indirect_Scherungssatz
then A3:
X is
Desarguesian
by AFF_2:25;
now let o,
a1,
a2,
a3,
a4,
b1,
b2,
b3,
b4 be
Element of
X;
:: thesis: for M, N being Subset of X st M is being_line & N is being_line & o in M & o in N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds
a3,a4 // b3,b4let M,
N be
Subset of
X;
:: thesis: ( M is being_line & N is being_line & o in M & o in N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 implies a3,a4 // b3,b4 )assume A4:
(
M is
being_line &
N is
being_line &
o in M &
o in N &
a1 in M &
a3 in M &
b2 in M &
b4 in M &
a2 in N &
a4 in N &
b1 in N &
b3 in N & not
a4 in M & not
a2 in M & not
b1 in M & not
b3 in M & not
a1 in N & not
a3 in N & not
b2 in N & not
b4 in N &
a3,
a2 // b3,
b2 &
a2,
a1 // b2,
b1 &
a1,
a4 // b1,
b4 )
;
:: thesis: a3,a4 // b3,b4then A5:
(
M // M &
N // N )
by AFF_1:55;
A6:
now assume A7:
(
a1 <> a3 &
a2 <> a4 )
;
:: thesis: a3,a4 // b3,b4A8:
b1 <> b3
proof
assume A9:
b1 = b3
;
:: thesis: contradiction
A10:
not
LIN o,
a2,
a1
by A4, AFF_1:39;
o,
a1 // o,
a3
by A4, A5, AFF_1:53;
then A11:
LIN o,
a1,
a3
by AFF_1:def 1;
b2,
b1 // a2,
a3
by A4, A9, AFF_1:13;
then
a2,
a1 // a2,
a3
by A4, AFF_1:14;
hence
contradiction
by A7, A10, A11, AFF_1:23;
:: thesis: verum
end;
ex
x,
y,
z being
Element of
X st
(
LIN x,
y,
z &
x <> y &
x <> z &
y <> z )
proof
assume A12:
for
x,
y,
z being
Element of
X holds
( not
LIN x,
y,
z or not
x <> y or not
x <> z or not
y <> z )
;
:: thesis: contradiction
o,
a1 // o,
a3
by A4, A5, AFF_1:53;
then
LIN o,
a1,
a3
by AFF_1:def 1;
hence
contradiction
by A4, A7, A12;
:: thesis: verum
end; then consider d being
Element of
X such that A13:
(
LIN a2,
a1,
d &
a2 <> d &
a1 <> d )
by A4, TRANSLAC:2;
A14:
o <> d
LIN o,
d,
d
by AFF_1:16;
then consider Y being
Subset of
X such that A15:
(
Y is
being_line &
o in Y &
d in Y &
d in Y )
by AFF_1:33;
ex
d1 being
Element of
X st
(
LIN b1,
b2,
d1 &
d1 in Y )
proof
consider e1 being
Element of
X such that A16:
(
b1,
b2 // b1,
e1 &
b1 <> e1 )
by DIRAF:47;
consider e2 being
Element of
X such that A17:
(
o,
d // o,
e2 &
o <> e2 )
by DIRAF:47;
not
b1,
e1 // o,
e2
proof
assume
b1,
e1 // o,
e2
;
:: thesis: contradiction
then
b1,
b2 // o,
e2
by A16, AFF_1:14;
then
b1,
b2 // o,
d
by A17, AFF_1:14;
then
b2,
b1 // o,
d
by AFF_1:13;
then A18:
a2,
a1 // o,
d
by A4, AFF_1:14;
a2,
a1 // a2,
d
by A13, AFF_1:def 1;
then
a2,
d // o,
d
by A4, A18, AFF_1:14;
then
d,
o // d,
a2
by AFF_1:13;
then
LIN d,
o,
a2
by AFF_1:def 1;
then A19:
LIN o,
a2,
d
by AFF_1:15;
A20:
not
LIN o,
a1,
a2
by A4, AFF_1:39;
LIN a1,
a2,
d
by A13, AFF_1:15;
then
a1,
a2 // a1,
d
by AFF_1:def 1;
hence
contradiction
by A13, A19, A20, AFF_1:23;
:: thesis: verum
end;
then consider d1 being
Element of
X such that A21:
(
LIN b1,
e1,
d1 &
LIN o,
e2,
d1 )
by AFF_1:74;
take
d1
;
:: thesis: ( LIN b1,b2,d1 & d1 in Y )
o,
e2 // o,
d1
by A21, AFF_1:def 1;
then
o,
d // o,
d1
by A17, AFF_1:14;
then A22:
LIN o,
d,
d1
by AFF_1:def 1;
b1,
e1 // b1,
d1
by A21, AFF_1:def 1;
then
b1,
b2 // b1,
d1
by A16, AFF_1:14;
hence
(
LIN b1,
b2,
d1 &
d1 in Y )
by A14, A15, A22, AFF_1:39, AFF_1:def 1;
:: thesis: verum
end; then consider d1 being
Element of
X such that A23:
(
LIN b1,
b2,
d1 &
d1 in Y )
;
ex
c1 being
Element of
X st
(
c1 in N &
a1,
a4 // b2,
c1 )
proof
consider e1 being
Element of
X such that A24:
(
a1,
a4 // b2,
e1 &
b2 <> e1 )
by DIRAF:47;
consider e2 being
Element of
X such that A25:
(
a2,
a4 // a2,
e2 &
a2 <> e2 )
by DIRAF:47;
not
b2,
e1 // a2,
e2
proof
assume
b2,
e1 // a2,
e2
;
:: thesis: contradiction
then
a1,
a4 // a2,
e2
by A24, AFF_1:14;
then
a1,
a4 // a2,
a4
by A25, AFF_1:14;
then
a4,
a2 // a4,
a1
by AFF_1:13;
then
LIN a4,
a2,
a1
by AFF_1:def 1;
hence
contradiction
by A4, A7, AFF_1:39;
:: thesis: verum
end;
then consider c1 being
Element of
X such that A26:
(
LIN b2,
e1,
c1 &
LIN a2,
e2,
c1 )
by AFF_1:74;
take
c1
;
:: thesis: ( c1 in N & a1,a4 // b2,c1 )
a2,
e2 // a2,
c1
by A26, AFF_1:def 1;
then
a2,
a4 // a2,
c1
by A25, AFF_1:14;
then A27:
LIN a2,
a4,
c1
by AFF_1:def 1;
b2,
e1 // b2,
c1
by A26, AFF_1:def 1;
hence
(
c1 in N &
a1,
a4 // b2,
c1 )
by A4, A7, A24, A27, AFF_1:14, AFF_1:39;
:: thesis: verum
end; then consider c1 being
Element of
X such that A28:
(
c1 in N &
a1,
a4 // b2,
c1 )
;
ex
c2 being
Element of
X st
(
c2 in M &
a2,
a3 // b1,
c2 )
proof
consider e1 being
Element of
X such that A29:
(
a2,
a3 // b1,
e1 &
b1 <> e1 )
by DIRAF:47;
consider e2 being
Element of
X such that A30:
(
a1,
a3 // a1,
e2 &
a1 <> e2 )
by DIRAF:47;
not
b1,
e1 // a1,
e2
proof
assume
b1,
e1 // a1,
e2
;
:: thesis: contradiction
then
a2,
a3 // a1,
e2
by A29, AFF_1:14;
then
a2,
a3 // a1,
a3
by A30, AFF_1:14;
then
a3,
a1 // a3,
a2
by AFF_1:13;
then
LIN a3,
a1,
a2
by AFF_1:def 1;
hence
contradiction
by A4, A7, AFF_1:39;
:: thesis: verum
end;
then consider c2 being
Element of
X such that A31:
(
LIN b1,
e1,
c2 &
LIN a1,
e2,
c2 )
by AFF_1:74;
take
c2
;
:: thesis: ( c2 in M & a2,a3 // b1,c2 )
a1,
e2 // a1,
c2
by A31, AFF_1:def 1;
then
a1,
a3 // a1,
c2
by A30, AFF_1:14;
then A32:
LIN a1,
a3,
c2
by AFF_1:def 1;
b1,
e1 // b1,
c2
by A31, AFF_1:def 1;
hence
(
c2 in M &
a2,
a3 // b1,
c2 )
by A4, A7, A29, A32, AFF_1:14, AFF_1:39;
:: thesis: verum
end; then consider c2 being
Element of
X such that A33:
(
c2 in M &
a2,
a3 // b1,
c2 )
;
A34:
(
M <> N &
M <> Y &
N <> Y )
a2,
d // b1,
d1
proof
A39:
(
a2,
a1 // a2,
d &
b1,
b2 // b1,
d1 )
by A13, A23, AFF_1:def 1;
then
b2,
b1 // b1,
d1
by AFF_1:13;
then
a2,
a1 // b1,
d1
by A4, AFF_1:14;
hence
a2,
d // b1,
d1
by A4, A39, AFF_1:14;
:: thesis: verum
end; then A40:
d,
a3 // d1,
c2
by A3, A4, A14, A15, A23, A33, A34, AFF_2:def 4;
a1,
d // b2,
d1
proof
(
LIN a1,
a2,
d &
LIN b2,
b1,
d1 )
by A13, A23, AFF_1:15;
then A41:
(
a1,
a2 // a1,
d &
b2,
b1 // b2,
d1 )
by AFF_1:def 1;
then
a2,
a1 // a1,
d
by AFF_1:13;
then
b2,
b1 // a1,
d
by A4, AFF_1:14;
hence
a1,
d // b2,
d1
by A4, A41, AFF_1:14;
:: thesis: verum
end; then
d,
a4 // d1,
c1
by A3, A4, A14, A15, A23, A28, A34, AFF_2:def 4;
then A42:
a3,
a4 // c2,
c1
by A3, A4, A14, A15, A23, A28, A33, A34, A40, AFF_2:def 4;
A43:
c1 <> c2
proof
assume
c1 = c2
;
:: thesis: contradiction
then
a3,
a2 // b1,
c1
by A33, AFF_1:13;
then A44:
b3,
b2 // b1,
c1
by A4, AFF_1:14;
A45:
b1 <> c1
proof
assume
b1 = c1
;
:: thesis: contradiction
then
a1,
a4 // a2,
a1
by A4, A28, AFF_1:14;
then
a1,
a4 // a1,
a2
by AFF_1:13;
then
LIN a1,
a4,
a2
by AFF_1:def 1;
then
LIN a2,
a4,
a1
by AFF_1:15;
hence
contradiction
by A4, A7, AFF_1:39;
:: thesis: verum
end;
b1,
c1 // b3,
b1
by A4, A5, A28, AFF_1:53;
then
b3,
b1 // b3,
b2
by A44, A45, AFF_1:14;
then
LIN b3,
b1,
b2
by AFF_1:def 1;
hence
contradiction
by A4, A8, AFF_1:39;
:: thesis: verum
end; A46:
(
o <> c1 &
o <> c2 )
proof
assume A47:
( not
o <> c1 or not
o <> c2 )
;
:: thesis: contradiction
A48:
now assume
o = c1
;
:: thesis: contradictionthen A49:
o,
b2 // a1,
a4
by A28, AFF_1:13;
o,
b2 // a1,
a3
by A4, A5, AFF_1:53;
then
a1,
a3 // a1,
a4
by A4, A49, AFF_1:14;
then
LIN a1,
a3,
a4
by AFF_1:def 1;
hence
contradiction
by A4, A7, AFF_1:39;
:: thesis: verum end;
now assume
o = c2
;
:: thesis: contradictionthen A50:
o,
b1 // a2,
a3
by A33, AFF_1:13;
o,
b1 // a2,
a4
by A4, A5, AFF_1:53;
then
a2,
a4 // a2,
a3
by A4, A50, AFF_1:14;
then
LIN a2,
a4,
a3
by AFF_1:def 1;
hence
contradiction
by A4, A7, AFF_1:39;
:: thesis: verum end;
hence
contradiction
by A47, A48;
:: thesis: verum
end;
b1,
b4 // b2,
c1
by A4, A28, AFF_1:14;
then A51:
b4,
b1 // b2,
c1
by AFF_1:13;
a3,
a2 // c2,
b1
by A33, AFF_1:13;
then
b3,
b2 // c2,
b1
by A4, AFF_1:14;
then
b2,
b3 // c2,
b1
by AFF_1:13;
then
b4,
b3 // c2,
c1
by A2, A4, A28, A33, A46, A51, AFF_2:def 2;
then
b4,
b3 // a3,
a4
by A42, A43, AFF_1:14;
hence
a3,
a4 // b3,
b4
by AFF_1:13;
:: thesis: verum end; now assume A52:
(
a1 = a3 or
a2 = a4 )
;
:: thesis: a3,a4 // b3,b4A53:
now assume A54:
a1 = a3
;
:: thesis: a3,a4 // b3,b4A55:
not
LIN o,
b2,
b1
by A4, AFF_1:39;
o,
b1 // o,
b3
by A4, A5, AFF_1:53;
then A56:
LIN o,
b1,
b3
by AFF_1:def 1;
a2,
a1 // b2,
b3
by A4, A54, AFF_1:13;
then
b2,
b1 // b2,
b3
by A4, AFF_1:14;
hence
a3,
a4 // b3,
b4
by A4, A54, A55, A56, AFF_1:23;
:: thesis: verum end; now assume A57:
a2 = a4
;
:: thesis: a3,a4 // b3,b4A58:
not
LIN o,
b1,
b2
by A4, AFF_1:39;
o,
b2 // o,
b4
by A4, A5, AFF_1:53;
then A59:
LIN o,
b2,
b4
by AFF_1:def 1;
a1,
a4 // b1,
b2
by A4, A57, AFF_1:13;
then
b1,
b2 // b1,
b4
by A4, AFF_1:14;
hence
a3,
a4 // b3,
b4
by A4, A57, A58, A59, AFF_1:23;
:: thesis: verum end; hence
a3,
a4 // b3,
b4
by A52, A53;
:: thesis: verum end; hence
a3,
a4 // b3,
b4
by A6;
:: thesis: verum end;
hence
X is
satisfying_major_indirect_Scherungssatz
by Def6;
:: thesis: verum
end;
( X is satisfying_major_indirect_Scherungssatz implies X is Pappian )
proof
assume A60:
X is
satisfying_major_indirect_Scherungssatz
;
:: thesis: X is Pappian
now let M,
N be
Subset of
X;
:: thesis: for o, a, b, c, a1, b1, c1 being Element of X st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & a in M & b in M & c in M & a1 in N & b1 in N & c1 in N & a,b1 // b,a1 & b,c1 // c,b1 holds
a,c1 // c,a1let o,
a,
b,
c,
a1,
b1,
c1 be
Element of
X;
:: thesis: ( M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & a in M & b in M & c in M & a1 in N & b1 in N & c1 in N & a,b1 // b,a1 & b,c1 // c,b1 implies a,c1 // c,a1 )assume A61:
(
M is
being_line &
N is
being_line &
M <> N &
o in M &
o in N &
o <> a &
o <> a1 &
o <> b &
o <> b1 &
o <> c &
o <> c1 &
a in M &
b in M &
c in M &
a1 in N &
b1 in N &
c1 in N &
a,
b1 // b,
a1 &
b,
c1 // c,
b1 )
;
:: thesis: a,c1 // c,a1A62:
( not
a in N & not
b in N & not
c in N & not
a1 in M & not
b1 in M & not
c1 in M )
proof
assume A63:
(
a in N or
b in N or
c in N or
a1 in M or
b1 in M or
c1 in M )
;
:: thesis: contradiction
(
o,
a // o,
a &
o,
b // o,
b &
o,
c // o,
c &
o,
a1 // o,
a1 &
o,
b1 // o,
b1 &
o,
c1 // o,
c1 )
by AFF_1:11;
then
M // N
by A61, A63, AFF_1:52;
hence
contradiction
by A61, AFF_1:59;
:: thesis: verum
end; A64:
(
a,
b1 // a1,
b &
b,
c1 // b1,
c )
by A61, AFF_1:13;
b1,
b // b,
b1
by AFF_1:11;
then
a,
c1 // a1,
c
by A60, A61, A62, A64, Def6;
hence
a,
c1 // c,
a1
by AFF_1:13;
:: thesis: verum end;
hence
X is
Pappian
by AFF_2:def 2;
:: thesis: verum
end;
hence
( X is Pappian iff X is satisfying_major_indirect_Scherungssatz )
by A1; :: thesis: verum