let X be OrtAfPl; :: thesis: ( 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
;
:: thesis: Af X is Pappian
now let M,
N be
Subset of
(Af X);
:: thesis: 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);
:: thesis: ( 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
;
:: thesis: a,c1 // c,a1reconsider a' =
a,
b' =
b,
c' =
c,
a1' =
a1,
b1' =
b1,
c1' =
c1 as
Element of
X by ANALMETR:47;
reconsider M' =
M,
N' =
N as
Subset of
X by ANALMETR:57;
A22:
N' is
being_line
by A4, ANALMETR:58;
A23:
( not
c1' in M' & not
b' in N' )
proof
assume
(
c1' in M' or
b' in N' )
;
:: thesis: 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;
:: thesis: verum
end;
b,
a1 // a,
b1
by A20, AFF_1:13;
then A26:
b',
a1' // a',
b1'
by ANALMETR:48;
A27:
b',
c1' // c',
b1'
by A21, ANALMETR:48;
M' is
being_line
by A3, ANALMETR:58;
then
a',
c1' // c',
a1'
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;
:: thesis: verum end;
hence
Af X is
Pappian
by AFF_2:def 2;
:: thesis: verum
end;
( Af X is Pappian implies X is satisfying_PAP )
proof
assume A28:
Af X is
Pappian
;
:: thesis: X is satisfying_PAP
now let o',
a1',
a2',
a3',
b1',
b2',
b3' be
Element of
X;
:: thesis: for M', N' being Subset of X st M' is being_line & N' is being_line & o' in M' & a1' in M' & a2' in M' & a3' in M' & o' in N' & b1' in N' & b2' in N' & b3' in N' & not b2' in M' & not a3' in N' & o' <> a1' & o' <> a2' & o' <> a3' & o' <> b1' & o' <> b2' & o' <> b3' & a3',b2' // a2',b1' & a3',b3' // a1',b1' holds
a1',b2' // a2',b3'let M',
N' be
Subset of
X;
:: thesis: ( M' is being_line & N' is being_line & o' in M' & a1' in M' & a2' in M' & a3' in M' & o' in N' & b1' in N' & b2' in N' & b3' in N' & not b2' in M' & not a3' in N' & o' <> a1' & o' <> a2' & o' <> a3' & o' <> b1' & o' <> b2' & o' <> b3' & a3',b2' // a2',b1' & a3',b3' // a1',b1' implies a1',b2' // a2',b3' )assume that A29:
M' is
being_line
and A30:
N' is
being_line
and A31:
o' in M'
and A32:
a1' in M'
and A33:
a2' in M'
and A34:
a3' in M'
and A35:
o' in N'
and A36:
b1' in N'
and A37:
b2' in N'
and A38:
b3' in N'
and A39:
not
b2' in M'
and A40:
not
a3' in N'
and A41:
o' <> a1'
and A42:
o' <> a2'
and
o' <> a3'
and A43:
o' <> b1'
and
o' <> b2'
and A44:
o' <> b3'
and A45:
a3',
b2' // a2',
b1'
and A46:
a3',
b3' // a1',
b1'
;
:: thesis: a1',b2' // a2',b3'reconsider a1 =
a1',
a2 =
a2',
a3 =
a3',
b1 =
b1',
b2 =
b2',
b3 =
b3' as
Element of
(Af X) by ANALMETR:47;
reconsider M =
M',
N =
N' 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
;
:: thesis: a1',b2' // a2',b3'
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
a1',
b2' // a2',
b3'
by ANALMETR:48;
:: thesis: verum end; hence
a1',
b2' // a2',
b3'
by A37, A39;
:: thesis: verum end;
hence
X is
satisfying_PAP
by CONMETR:def 2;
:: thesis: verum
end;
hence
( X is satisfying_PAP iff Af X is Pappian )
by A1; :: thesis: verum