let X be OrtAfPl; ( X is satisfying_PAP iff Af X is Pappian )
A1:
( X is satisfying_PAP implies Af X is Pappian )
proof
assume A2:
X is
satisfying_PAP
;
Af X is Pappian
now let M,
N be
Subset of
(Af X);
for o, a, b, c, a1, b1, c1 being Element of (Af 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
(Af X);
( 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 that A3:
M is
being_line
and A4:
N is
being_line
and A5:
M <> N
and A6:
o in M
and A7:
o in N
and A8:
o <> a
and A9:
o <> a1
and A10:
o <> b
and A11:
o <> b1
and A12:
o <> c
and A13:
o <> c1
and A14:
a in M
and A15:
b in M
and A16:
c in M
and A17:
a1 in N
and A18:
b1 in N
and A19:
c1 in N
and A20:
a,
b1 // b,
a1
and A21:
b,
c1 // c,
b1
;
a,c1 // c,a1reconsider a9 =
a,
b9 =
b,
c9 =
c,
a19 =
a1,
b19 =
b1,
c19 =
c1 as
Element of
X by ANALMETR:47;
reconsider M9 =
M,
N9 =
N as
Subset of
X by ANALMETR:57;
A22:
N9 is
being_line
by A4, ANALMETR:58;
A23:
( not
c19 in M9 & not
b9 in N9 )
proof
assume
(
c19 in M9 or
b9 in N9 )
;
contradiction
then A24:
(
o,
c1 // M or
o,
b // N )
by A3, A4, A6, A7, AFF_1:66;
A25:
o,
b // M
by A3, A6, A15, AFF_1:66;
o,
c1 // N
by A4, A7, A19, AFF_1:66;
hence
contradiction
by A5, A6, A7, A10, A13, A24, A25, AFF_1:59, AFF_1:67;
verum
end;
b,
a1 // a,
b1
by A20, AFF_1:13;
then A26:
b9,
a19 // a9,
b19
by ANALMETR:48;
A27:
b9,
c19 // c9,
b19
by A21, ANALMETR:48;
M9 is
being_line
by A3, ANALMETR:58;
then
a9,
c19 // c9,
a19
by A2, A6, A7, A8, A9, A11, A12, A14, A15, A16, A17, A18, A19, A22, A26, A27, A23, CONMETR:def 2;
hence
a,
c1 // c,
a1
by ANALMETR:48;
verum end;
hence
Af X is
Pappian
by AFF_2:def 2;
verum
end;
( Af X is Pappian implies X is satisfying_PAP )
proof
assume A28:
Af X is
Pappian
;
X is satisfying_PAP
now let o9,
a19,
a29,
a39,
b19,
b29,
b39 be
Element of
X;
for M9, N9 being Subset of X st M9 is being_line & N9 is being_line & o9 in M9 & a19 in M9 & a29 in M9 & a39 in M9 & o9 in N9 & b19 in N9 & b29 in N9 & b39 in N9 & not b29 in M9 & not a39 in N9 & o9 <> a19 & o9 <> a29 & o9 <> a39 & o9 <> b19 & o9 <> b29 & o9 <> b39 & a39,b29 // a29,b19 & a39,b39 // a19,b19 holds
a19,b29 // a29,b39let M9,
N9 be
Subset of
X;
( M9 is being_line & N9 is being_line & o9 in M9 & a19 in M9 & a29 in M9 & a39 in M9 & o9 in N9 & b19 in N9 & b29 in N9 & b39 in N9 & not b29 in M9 & not a39 in N9 & o9 <> a19 & o9 <> a29 & o9 <> a39 & o9 <> b19 & o9 <> b29 & o9 <> b39 & a39,b29 // a29,b19 & a39,b39 // a19,b19 implies a19,b29 // a29,b39 )assume that A29:
M9 is
being_line
and A30:
N9 is
being_line
and A31:
o9 in M9
and A32:
a19 in M9
and A33:
a29 in M9
and A34:
a39 in M9
and A35:
o9 in N9
and A36:
b19 in N9
and A37:
b29 in N9
and A38:
b39 in N9
and A39:
not
b29 in M9
and A40:
not
a39 in N9
and A41:
o9 <> a19
and A42:
o9 <> a29
and
o9 <> a39
and A43:
o9 <> b19
and
o9 <> b29
and A44:
o9 <> b39
and A45:
a39,
b29 // a29,
b19
and A46:
a39,
b39 // a19,
b19
;
a19,b29 // a29,b39reconsider a1 =
a19,
a2 =
a29,
a3 =
a39,
b1 =
b19,
b2 =
b29,
b3 =
b39 as
Element of
(Af X) by ANALMETR:47;
reconsider M =
M9,
N =
N9 as
Subset of
(Af X) by ANALMETR:57;
A47:
N is
being_line
by A30, ANALMETR:58;
A48:
M is
being_line
by A29, ANALMETR:58;
now assume
M <> N
;
a19,b29 // a29,b39
a3,
b3 // a1,
b1
by A46, ANALMETR:48;
then A49:
a1,
b1 // a3,
b3
by AFF_1:13;
a3,
b2 // a2,
b1
by A45, ANALMETR:48;
then
a1,
b2 // a2,
b3
by A28, A31, A32, A33, A34, A35, A36, A37, A38, A39, A40, A41, A42, A43, A44, A48, A47, A49, AFF_2:def 2;
hence
a19,
b29 // a29,
b39
by ANALMETR:48;
verum end; hence
a19,
b29 // a29,
b39
by A37, A39;
verum end;
hence
X is
satisfying_PAP
by CONMETR:def 2;
verum
end;
hence
( X is satisfying_PAP iff Af X is Pappian )
by A1; verum