let X be AffinPlane; ( X is satisfying_pap iff X is satisfying_minor_indirect_Scherungssatz )
A1:
( X is satisfying_minor_indirect_Scherungssatz implies X is satisfying_pap )
proof
assume A2:
X is
satisfying_minor_indirect_Scherungssatz
;
X is satisfying_pap
now for M, N being Subset of X
for a, b, c, a1, b1, c1 being Element of X st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a1 in N & b1 in N & c1 in N & a,b1 // b,a1 & b,c1 // c,b1 holds
a,c1 // c,a1let M,
N be
Subset of
X;
for a, b, c, a1, b1, c1 being Element of X st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a1 in N & b1 in N & c1 in N & a,b1 // b,a1 & b,c1 // c,b1 holds
a,c1 // c,a1let a,
b,
c,
a1,
b1,
c1 be
Element of
X;
( M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a1 in N & b1 in N & c1 in N & a,b1 // b,a1 & b,c1 // c,b1 implies a,c1 // c,a1 )assume that
M is
being_line
and
N is
being_line
and A3:
a in M
and A4:
b in M
and A5:
c in M
and A6:
M // N
and A7:
M <> N
and A8:
a1 in N
and A9:
b1 in N
and A10:
c1 in N
and A11:
a,
b1 // b,
a1
and A12:
b,
c1 // c,
b1
;
a,c1 // c,a1A13:
not
b in N
by A4, A6, A7, AFF_1:45;
A14:
not
c1 in M
by A6, A7, A10, AFF_1:45;
A15:
not
c in N
by A5, A6, A7, AFF_1:45;
A16:
b1,
b // b,
b1
by AFF_1:2;
A17:
not
b1 in M
by A6, A7, A9, AFF_1:45;
A18:
b,
c1 // b1,
c
by A12, AFF_1:4;
A19:
not
a1 in M
by A6, A7, A8, AFF_1:45;
A20:
a,
b1 // a1,
b
by A11, AFF_1:4;
not
a in N
by A3, A6, A7, AFF_1:45;
then
a,
c1 // a1,
c
by A2, A3, A4, A5, A6, A8, A9, A10, A13, A15, A19, A17, A14, A20, A18, A16;
hence
a,
c1 // c,
a1
by AFF_1:4;
verum end;
hence
X is
satisfying_pap
by AFF_2:def 13;
verum
end;
( X is satisfying_pap implies X is satisfying_minor_indirect_Scherungssatz )
proof
assume A21:
X is
satisfying_pap
;
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 A22:
M // N
and A23:
a1 in M
and A24:
a3 in M
and A25:
b2 in M
and A26:
b4 in M
and A27:
a2 in N
and A28:
a4 in N
and A29:
b1 in N
and A30:
b3 in N
and A31:
not
a4 in M
and
not
a2 in M
and
not
b1 in M
and
not
b3 in M
and
not
a1 in N
and
not
a3 in N
and
not
b2 in N
and
not
b4 in N
and A32:
a3,
a2 // b3,
b2
and A33:
a2,
a1 // b2,
b1
and A34:
a1,
a4 // b1,
b4
;
a3,a4 // b3,b4A35:
M is
being_line
by A22, AFF_1:36;
A36:
b2,
b3 // a3,
a2
by A32, AFF_1:4;
A37:
N is
being_line
by A22, AFF_1:36;
A38:
a4,
a1 // b1,
b4
by A34, AFF_1:4;
a1,
a2 // b2,
b1
by A33, AFF_1:4;
then
a1,
b3 // a3,
b1
by A21, A22, A23, A24, A25, A27, A28, A29, A30, A31, A35, A37, A36, AFF_2:def 13;
then
b1,
a3 // b3,
a1
by AFF_1:4;
then
a4,
a3 // b3,
b4
by A21, A22, A23, A24, A26, A28, A29, A30, A31, A35, A37, A38, AFF_2:def 13;
hence
a3,
a4 // b3,
b4
by AFF_1:4;
verum end;
hence
X is
satisfying_minor_indirect_Scherungssatz
;
verum
end;
hence
( X is satisfying_pap iff X is satisfying_minor_indirect_Scherungssatz )
by A1; verum