let X be AffinPlane; ( X is satisfying_minor_indirect_Scherungssatz implies X is satisfying_minor_Scherungssatz )
assume A1:
X is satisfying_minor_indirect_Scherungssatz
; X is satisfying_minor_Scherungssatz
now for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X st M // 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 a1,
a2,
a3,
a4,
b1,
b2,
b3,
b4 be
Element of
X;
for M, N being Subset of X st M // 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 // 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 // N
and A3:
a1 in M
and A4:
a3 in M
and A5:
b1 in M
and A6:
b3 in M
and A7:
a2 in N
and A8:
a4 in N
and A9:
b2 in N
and A10:
b4 in N
and A11:
not
a4 in M
and A12:
not
a2 in M
and A13:
not
b2 in M
and A14:
not
b4 in M
and A15:
not
a1 in N
and A16:
not
a3 in N
and A17:
not
b1 in N
and A18:
not
b3 in N
and A19:
a3,
a2 // b3,
b2
and A20:
a2,
a1 // b2,
b1
and A21:
a1,
a4 // b1,
b4
;
a3,a4 // b3,b4A22:
N is
being_line
by A2, AFF_1:36;
then consider d1 being
Element of
X such that
a2 <> d1
and A23:
d1 in N
by AFF_1:20;
A24:
not
d1 in M
by A2, A8, A11, A23, AFF_1:45;
A25:
M is
being_line
by A2, AFF_1:36;
ex
d2 being
Element of
X st
(
d2 in M &
a2,
a1 // d2,
d1 )
proof
consider e1 being
Element of
X such that A26:
a1 <> e1
and A27:
e1 in M
by A25, AFF_1:20;
consider e2 being
Element of
X such that A28:
a2,
a1 // d1,
e2
and A29:
d1 <> e2
by DIRAF:40;
not
a1,
e1 // d1,
e2
proof
assume
a1,
e1 // d1,
e2
;
contradiction
then
a1,
e1 // a2,
a1
by A28, A29, AFF_1:5;
then
a1,
e1 // a1,
a2
by AFF_1:4;
then
LIN a1,
e1,
a2
by AFF_1:def 1;
hence
contradiction
by A3, A12, A25, A26, A27, AFF_1:25;
verum
end;
then consider d2 being
Element of
X such that A30:
LIN a1,
e1,
d2
and A31:
LIN d1,
e2,
d2
by AFF_1:60;
take
d2
;
( d2 in M & a2,a1 // d2,d1 )
d1,
e2 // d1,
d2
by A31, AFF_1:def 1;
then
a2,
a1 // d1,
d2
by A28, A29, AFF_1:5;
hence
(
d2 in M &
a2,
a1 // d2,
d1 )
by A3, A25, A26, A27, A30, AFF_1:4, AFF_1:25;
verum
end; then consider d2 being
Element of
X such that A32:
d2 in M
and A33:
a2,
a1 // d2,
d1
;
A34:
not
d2 in N
by A2, A8, A11, A32, AFF_1:45;
ex
d3 being
Element of
X st
(
d3 in N &
a3,
a2 // d3,
d2 )
proof
consider e1 being
Element of
X such that A35:
a2 <> e1
and A36:
e1 in N
by A22, AFF_1:20;
consider e2 being
Element of
X such that A37:
a3,
a2 // d2,
e2
and A38:
d2 <> e2
by DIRAF:40;
not
a2,
e1 // d2,
e2
proof
assume
a2,
e1 // d2,
e2
;
contradiction
then
a2,
e1 // a3,
a2
by A37, A38, AFF_1:5;
then
a2,
e1 // a2,
a3
by AFF_1:4;
then
LIN a2,
e1,
a3
by AFF_1:def 1;
hence
contradiction
by A7, A16, A22, A35, A36, AFF_1:25;
verum
end;
then consider d3 being
Element of
X such that A39:
LIN a2,
e1,
d3
and A40:
LIN d2,
e2,
d3
by AFF_1:60;
take
d3
;
( d3 in N & a3,a2 // d3,d2 )
d2,
e2 // d2,
d3
by A40, AFF_1:def 1;
then
a3,
a2 // d2,
d3
by A37, A38, AFF_1:5;
hence
(
d3 in N &
a3,
a2 // d3,
d2 )
by A7, A22, A35, A36, A39, AFF_1:4, AFF_1:25;
verum
end; then consider d3 being
Element of
X such that A41:
d3 in N
and A42:
a3,
a2 // d3,
d2
;
A43:
not
d3 in M
by A2, A8, A11, A41, AFF_1:45;
ex
d4 being
Element of
X st
(
d4 in M &
a1,
a4 // d1,
d4 )
proof
consider e1 being
Element of
X such that A44:
a1 <> e1
and A45:
e1 in M
by A25, AFF_1:20;
consider e2 being
Element of
X such that A46:
a1,
a4 // d1,
e2
and A47:
d1 <> e2
by DIRAF:40;
not
a1,
e1 // d1,
e2
proof
assume
a1,
e1 // d1,
e2
;
contradiction
then
a1,
e1 // a1,
a4
by A46, A47, AFF_1:5;
then
LIN a1,
e1,
a4
by AFF_1:def 1;
hence
contradiction
by A3, A11, A25, A44, A45, AFF_1:25;
verum
end;
then consider d4 being
Element of
X such that A48:
LIN a1,
e1,
d4
and A49:
LIN d1,
e2,
d4
by AFF_1:60;
take
d4
;
( d4 in M & a1,a4 // d1,d4 )
d1,
e2 // d1,
d4
by A49, AFF_1:def 1;
hence
(
d4 in M &
a1,
a4 // d1,
d4 )
by A3, A25, A44, A45, A46, A47, A48, AFF_1:5, AFF_1:25;
verum
end; then consider d4 being
Element of
X such that A50:
d4 in M
and A51:
a1,
a4 // d1,
d4
;
A52:
not
d4 in N
by A2, A8, A11, A50, AFF_1:45;
A53:
b2,
b1 // d2,
d1
by A3, A12, A20, A33, AFF_1:5;
A54:
b1,
b4 // d1,
d4
by A3, A11, A21, A51, AFF_1:5;
b3,
b2 // d3,
d2
by A4, A12, A19, A42, AFF_1:5;
then A55:
b3,
b4 // d3,
d4
by A1, A2, A5, A6, A9, A10, A13, A14, A17, A18, A23, A32, A41, A50, A24, A43, A34, A52, A53, A54;
a3,
a4 // d3,
d4
by A1, A2, A3, A4, A7, A8, A11, A12, A15, A16, A23, A32, A33, A41, A42, A50, A51, A24, A43, A34, A52;
hence
a3,
a4 // b3,
b4
by A50, A43, A55, AFF_1:5;
verum end;
hence
X is satisfying_minor_Scherungssatz
; verum