let X be AffinPlane; ( X is satisfying_major_indirect_Scherungssatz implies X is satisfying_major_Scherungssatz )
assume A1:
X is satisfying_major_indirect_Scherungssatz
; X is satisfying_major_Scherungssatz
now for o, a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
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 & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds
a3,a4 // b3,b4let o,
a1,
a2,
a3,
a4,
b1,
b2,
b3,
b4 be
Element of
X;
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 & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 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;
( M is being_line & N is being_line & o in M & o in N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 implies a3,a4 // b3,b4 )assume that A2:
M is
being_line
and A3:
N is
being_line
and A4:
o in M
and A5:
o in N
and A6:
a1 in M
and A7:
a3 in M
and A8:
b1 in M
and A9:
b3 in M
and A10:
a2 in N
and A11:
a4 in N
and A12:
b2 in N
and A13:
b4 in N
and A14:
not
a4 in M
and A15:
not
a2 in M
and A16:
not
b2 in M
and A17:
not
b4 in M
and A18:
not
a1 in N
and A19:
not
a3 in N
and A20:
not
b1 in N
and A21:
not
b3 in N
and A22:
a3,
a2 // b3,
b2
and A23:
a2,
a1 // b2,
b1
and A24:
a1,
a4 // b1,
b4
;
a3,a4 // b3,b4A25:
now ( a1 <> a3 & a2 <> a4 implies a3,a4 // b3,b4 )assume that A26:
a1 <> a3
and A27:
a2 <> a4
;
a3,a4 // b3,b4consider d1 being
Element of
X such that A28:
o <> d1
and A29:
d1 in N
by A4, A11, A14;
A30:
ex
d4 being
Element of
X st
(
d4 in M &
a1,
a4 // d1,
d4 )
proof
consider e1 being
Element of
X such that A31:
o <> e1
and A32:
e1 in M
by A5, A6, A18;
consider e2 being
Element of
X such that A33:
a1,
a4 // d1,
e2
and A34:
d1 <> e2
by DIRAF:40;
not
o,
e1 // d1,
e2
proof
assume
o,
e1 // d1,
e2
;
contradiction
then A35:
o,
e1 // a1,
a4
by A33, A34, AFF_1:5;
o,
e1 // a1,
a3
by A2, A4, A6, A7, A32, AFF_1:39, AFF_1:41;
then
a1,
a3 // a1,
a4
by A31, A35, AFF_1:5;
then
LIN a1,
a3,
a4
by AFF_1:def 1;
hence
contradiction
by A2, A6, A7, A14, A26, AFF_1:25;
verum
end;
then consider d4 being
Element of
X such that A36:
LIN o,
e1,
d4
and A37:
LIN d1,
e2,
d4
by AFF_1:60;
take
d4
;
( d4 in M & a1,a4 // d1,d4 )
d1,
e2 // d1,
d4
by A37, AFF_1:def 1;
hence
(
d4 in M &
a1,
a4 // d1,
d4 )
by A2, A4, A31, A32, A33, A34, A36, AFF_1:5, AFF_1:25;
verum
end; A38:
ex
d2 being
Element of
X st
(
d2 in M &
a2,
a1 // d2,
d1 )
proof
consider e1 being
Element of
X such that A39:
o <> e1
and A40:
e1 in M
by A5, A6, A18;
consider e2 being
Element of
X such that A41:
a2,
a1 // d1,
e2
and A42:
d1 <> e2
by DIRAF:40;
not
o,
e1 // d1,
e2
proof
assume
o,
e1 // d1,
e2
;
contradiction
then A43:
o,
e1 // a2,
a1
by A41, A42, AFF_1:5;
o,
e1 // a1,
a3
by A2, A4, A6, A7, A40, AFF_1:39, AFF_1:41;
then
a1,
a3 // a2,
a1
by A39, A43, AFF_1:5;
then
a1,
a3 // a1,
a2
by AFF_1:4;
then
LIN a1,
a3,
a2
by AFF_1:def 1;
hence
contradiction
by A2, A6, A7, A15, A26, AFF_1:25;
verum
end;
then consider d2 being
Element of
X such that A44:
LIN o,
e1,
d2
and A45:
LIN d1,
e2,
d2
by AFF_1:60;
take
d2
;
( d2 in M & a2,a1 // d2,d1 )
d1,
e2 // d1,
d2
by A45, AFF_1:def 1;
then
a2,
a1 // d1,
d2
by A41, A42, AFF_1:5;
hence
(
d2 in M &
a2,
a1 // d2,
d1 )
by A2, A4, A39, A40, A44, AFF_1:4, AFF_1:25;
verum
end; consider d4 being
Element of
X such that A46:
d4 in M
and A47:
a1,
a4 // d1,
d4
by A30;
consider d2 being
Element of
X such that A48:
d2 in M
and A49:
a2,
a1 // d2,
d1
by A38;
A50:
b2,
b1 // d2,
d1
by A6, A15, A23, A49, AFF_1:5;
ex
d3 being
Element of
X st
(
d3 in N &
a3,
a2 // d3,
d2 )
proof
consider e1 being
Element of
X such that A51:
o <> e1
and A52:
e1 in N
by A4, A11, A14;
consider e2 being
Element of
X such that A53:
a3,
a2 // d2,
e2
and A54:
d2 <> e2
by DIRAF:40;
not
o,
e1 // d2,
e2
proof
assume
o,
e1 // d2,
e2
;
contradiction
then A55:
o,
e1 // a3,
a2
by A53, A54, AFF_1:5;
o,
e1 // a2,
a4
by A3, A5, A10, A11, A52, AFF_1:39, AFF_1:41;
then
a2,
a4 // a3,
a2
by A51, A55, AFF_1:5;
then
a2,
a4 // a2,
a3
by AFF_1:4;
then
LIN a2,
a4,
a3
by AFF_1:def 1;
hence
contradiction
by A3, A10, A11, A19, A27, AFF_1:25;
verum
end;
then consider d3 being
Element of
X such that A56:
LIN o,
e1,
d3
and A57:
LIN d2,
e2,
d3
by AFF_1:60;
take
d3
;
( d3 in N & a3,a2 // d3,d2 )
d2,
e2 // d2,
d3
by A57, AFF_1:def 1;
then
a3,
a2 // d2,
d3
by A53, A54, AFF_1:5;
hence
(
d3 in N &
a3,
a2 // d3,
d2 )
by A3, A5, A51, A52, A56, AFF_1:4, AFF_1:25;
verum
end; then consider d3 being
Element of
X such that A58:
d3 in N
and A59:
a3,
a2 // d3,
d2
;
A60:
(
d2 <> o &
d3 <> o &
d4 <> o )
proof
A61:
now not d4 = oassume A62:
d4 = o
;
contradiction
d1,
o // a2,
a4
by A3, A5, A10, A11, A29, AFF_1:39, AFF_1:41;
then
a1,
a4 // a2,
a4
by A28, A47, A62, AFF_1:5;
then
a4,
a2 // a4,
a1
by AFF_1:4;
then
LIN a4,
a2,
a1
by AFF_1:def 1;
hence
contradiction
by A3, A10, A11, A18, A27, AFF_1:25;
verum end;
A63:
now not d2 = oassume A64:
d2 = o
;
contradiction
o,
d1 // a2,
a4
by A3, A5, A10, A11, A29, AFF_1:39, AFF_1:41;
then
a2,
a4 // a2,
a1
by A28, A49, A64, AFF_1:5;
then
LIN a2,
a4,
a1
by AFF_1:def 1;
hence
contradiction
by A3, A10, A11, A18, A27, AFF_1:25;
verum end;
A65:
now not d3 = oassume A66:
d3 = o
;
contradiction
o,
d2 // a3,
a1
by A2, A4, A6, A7, A48, AFF_1:39, AFF_1:41;
then
a3,
a1 // a3,
a2
by A59, A63, A66, AFF_1:5;
then
LIN a3,
a1,
a2
by AFF_1:def 1;
hence
contradiction
by A2, A6, A7, A15, A26, AFF_1:25;
verum end;
assume
( not
d2 <> o or not
d3 <> o or not
d4 <> o )
;
contradiction
hence
contradiction
by A63, A65, A61;
verum
end; A67:
( not
d1 in M & not
d3 in M & not
d2 in N & not
d4 in N )
proof
assume
(
d1 in M or
d3 in M or
d2 in N or
d4 in N )
;
contradiction
then A68:
(
o,
d1 // M or
o,
d3 // M or
o,
d2 // N or
o,
d4 // N )
by A2, A3, A4, A5, AFF_1:52;
A69:
o,
d3 // N
by A3, A5, A58, AFF_1:52;
A70:
o,
d4 // M
by A2, A4, A46, AFF_1:52;
A71:
o,
d2 // M
by A2, A4, A48, AFF_1:52;
o,
d1 // N
by A3, A5, A29, AFF_1:52;
hence
contradiction
by A4, A5, A11, A14, A28, A60, A68, A69, A71, A70, AFF_1:45, AFF_1:53;
verum
end; A72:
b1,
b4 // d1,
d4
by A6, A14, A24, A47, AFF_1:5;
A73:
(
d1 <> d2 &
d2 <> d3 &
d3 <> d4 &
d4 <> d1 )
proof
assume
( not
d1 <> d2 or not
d2 <> d3 or not
d3 <> d4 or not
d4 <> d1 )
;
contradiction
then A74:
(
o,
d1 // M or
o,
d3 // M )
by A2, A4, A48, A46, AFF_1:52;
A75:
o,
d3 // N
by A3, A5, A58, AFF_1:52;
o,
d1 // N
by A3, A5, A29, AFF_1:52;
hence
contradiction
by A4, A5, A11, A14, A28, A60, A74, A75, AFF_1:45, AFF_1:53;
verum
end;
b3,
b2 // d3,
d2
by A7, A15, A22, A59, AFF_1:5;
then A76:
b3,
b4 // d3,
d4
by A1, A2, A3, A4, A5, A8, A9, A12, A13, A16, A17, A20, A21, A29, A48, A58, A46, A67, A50, A72;
a3,
a4 // d3,
d4
by A1, A2, A3, A4, A5, A6, A7, A10, A11, A14, A15, A18, A19, A29, A48, A49, A58, A59, A46, A47, A67;
hence
a3,
a4 // b3,
b4
by A73, A76, AFF_1:5;
verum end; now ( ( a1 = a3 or a2 = a4 ) implies a3,a4 // b3,b4 )A77:
now ( a2 = a4 implies a3,a4 // b3,b4 )
o,
b2 // o,
b4
by A3, A5, A12, A13, AFF_1:39, AFF_1:41;
then A78:
LIN o,
b2,
b4
by AFF_1:def 1;
assume A79:
a2 = a4
;
a3,a4 // b3,b4then
a1,
a4 // b1,
b2
by A23, AFF_1:4;
then
b1,
b2 // b1,
b4
by A6, A14, A24, AFF_1:5;
hence
a3,
a4 // b3,
b4
by A2, A4, A5, A8, A16, A20, A22, A79, A78, AFF_1:14, AFF_1:25;
verum end; A80:
now ( a1 = a3 implies a3,a4 // b3,b4 )
o,
b1 // o,
b3
by A2, A4, A8, A9, AFF_1:39, AFF_1:41;
then A81:
LIN o,
b1,
b3
by AFF_1:def 1;
assume A82:
a1 = a3
;
a3,a4 // b3,b4then
a2,
a1 // b2,
b3
by A22, AFF_1:4;
then
b2,
b1 // b2,
b3
by A6, A15, A23, AFF_1:5;
hence
a3,
a4 // b3,
b4
by A3, A4, A5, A12, A16, A20, A24, A82, A81, AFF_1:14, AFF_1:25;
verum end; assume
(
a1 = a3 or
a2 = a4 )
;
a3,a4 // b3,b4hence
a3,
a4 // b3,
b4
by A80, A77;
verum end; hence
a3,
a4 // b3,
b4
by A25;
verum end;
hence
X is satisfying_major_Scherungssatz
; verum