let X be AffinPlane; ( X is satisfying_indirect_Scherungssatz iff ( X is satisfying_minor_indirect_Scherungssatz & X is satisfying_major_indirect_Scherungssatz ) )
A1:
( X is satisfying_indirect_Scherungssatz implies X is satisfying_minor_indirect_Scherungssatz )
proof
assume A2:
X is
satisfying_indirect_Scherungssatz
;
X is satisfying_minor_indirect_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 & 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 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 & 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;
( M // 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 that A3:
M // N
and A4:
a1 in M
and A5:
a3 in M
and A6:
b2 in M
and A7:
b4 in M
and A8:
a2 in N
and A9:
a4 in N
and A10:
b1 in N
and A11:
b3 in N
and A12:
not
a4 in M
and A13:
not
a2 in M
and A14:
not
b1 in M
and A15:
not
b3 in M
and A16:
not
a1 in N
and A17:
not
a3 in N
and A18:
not
b2 in N
and A19:
not
b4 in N
and A20:
a3,
a2 // b3,
b2
and A21:
a2,
a1 // b2,
b1
and A22:
a1,
a4 // b1,
b4
;
a3,a4 // b3,b4A23:
N is
being_line
by A3, AFF_1:36;
M is
being_line
by A3, AFF_1:36;
hence
a3,
a4 // b3,
b4
by A2, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A21, A22, A23;
verum end;
hence
X is
satisfying_minor_indirect_Scherungssatz
;
verum
end;
A24:
( X is satisfying_minor_indirect_Scherungssatz & X is satisfying_major_indirect_Scherungssatz implies X is satisfying_indirect_Scherungssatz )
proof
assume that A25:
X is
satisfying_minor_indirect_Scherungssatz
and A26:
X is
satisfying_major_indirect_Scherungssatz
;
X is satisfying_indirect_Scherungssatz
now for 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 & 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 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 & 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;
( M is being_line & N is being_line & 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 that A27:
M is
being_line
and A28:
N is
being_line
and A29:
a1 in M
and A30:
a3 in M
and A31:
b2 in M
and A32:
b4 in M
and A33:
a2 in N
and A34:
a4 in N
and A35:
b1 in N
and A36:
b3 in N
and A37:
not
a4 in M
and A38:
not
a2 in M
and A39:
not
b1 in M
and A40:
not
b3 in M
and A41:
not
a1 in N
and A42:
not
a3 in N
and A43:
not
b2 in N
and A44:
not
b4 in N
and A45:
a3,
a2 // b3,
b2
and A46:
a2,
a1 // b2,
b1
and A47:
a1,
a4 // b1,
b4
;
a3,a4 // b3,b4now ( not M // N implies a3,a4 // b3,b4 )assume
not
M // N
;
a3,a4 // b3,b4then
ex
o being
Element of
X st
(
o in M &
o in N )
by A27, A28, AFF_1:58;
hence
a3,
a4 // b3,
b4
by A26, A27, A28, A29, A30, A31, A32, A33, A34, A35, A36, A37, A38, A39, A40, A41, A42, A43, A44, A45, A46, A47;
verum end; hence
a3,
a4 // b3,
b4
by A25, A29, A30, A31, A32, A33, A34, A35, A36, A37, A38, A39, A40, A41, A42, A43, A44, A45, A46, A47;
verum end;
hence
X is
satisfying_indirect_Scherungssatz
;
verum
end;
thus
( X is satisfying_indirect_Scherungssatz iff ( X is satisfying_minor_indirect_Scherungssatz & X is satisfying_major_indirect_Scherungssatz ) )
by A1, A24; verum