let MS be OrtAfPl; ( MS is satisfying_PAP iff AffinStruct(# the carrier of MS, the CONGR of MS #) is Pappian )
set AS = AffinStruct(# the carrier of MS, the CONGR of MS #);
A1:
now ( MS is satisfying_PAP implies AffinStruct(# the carrier of MS, the CONGR of MS #) is Pappian )assume A2:
MS is
satisfying_PAP
;
AffinStruct(# the carrier of MS, the CONGR of MS #) is Pappian now for M, N being Subset of AffinStruct(# the carrier of MS, the CONGR of MS #)
for o, a, b, c, a9, b9, c9 being Element of AffinStruct(# the carrier of MS, the CONGR of MS #) st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9let M,
N be
Subset of
AffinStruct(# the
carrier of
MS, the
CONGR of
MS #);
for o, a, b, c, a9, b9, c9 being Element of AffinStruct(# the carrier of MS, the CONGR of MS #) st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9let o,
a,
b,
c,
a9,
b9,
c9 be
Element of
AffinStruct(# the
carrier of
MS, the
CONGR of
MS #);
( M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 implies a,c9 // c,a9 )assume that A3:
(
M is
being_line &
N is
being_line )
and A4:
M <> N
and A5:
(
o in M &
o in N )
and A6:
o <> a
and A7:
(
o <> a9 &
o <> b )
and A8:
(
o <> b9 &
o <> c &
o <> c9 &
a in M )
and A9:
b in M
and A10:
c in M
and A11:
a9 in N
and A12:
(
b9 in N &
c9 in N )
and A13:
a,
b9 // b,
a9
and A14:
b,
c9 // c,
b9
;
a,c9 // c,a9reconsider M9 =
M,
N9 =
N as
Subset of
MS ;
reconsider a1 =
a,
b1 =
b,
c1 =
c,
a19 =
a9,
b19 =
b9,
c19 =
c9 as
Element of
MS ;
A15:
b1,
c19 // c1,
b19
by A14, ANALMETR:36;
a1,
b19 // b1,
a19
by A13, ANALMETR:36;
then A16:
b1,
a19 // a1,
b19
by ANALMETR:59;
A17:
(
M9 is
being_line &
N9 is
being_line )
by A3, ANALMETR:43;
then
( not
a19 in M9 & not
b1 in N9 )
by A4, A5, A7, A9, A11, CONMETR:5;
then
c1,
a19 // a1,
c19
by A2, A5, A6, A8, A9, A10, A11, A12, A17, A16, A15, CONMETR:def 2;
then
a1,
c19 // c1,
a19
by ANALMETR:59;
hence
a,
c9 // c,
a9
by ANALMETR:36;
verum end; hence
AffinStruct(# the
carrier of
MS, the
CONGR of
MS #) is
Pappian
by AFF_2:def 2;
verum end;
now ( AffinStruct(# the carrier of MS, the CONGR of MS #) is Pappian implies MS is satisfying_PAP )assume A18:
AffinStruct(# the
carrier of
MS, the
CONGR of
MS #) is
Pappian
;
MS is satisfying_PAP now for o, a1, a2, a3, b1, b2, b3 being Element of MS
for M, N being Subset of the carrier of MS 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,b3let o,
a1,
a2,
a3,
b1,
b2,
b3 be
Element of
MS;
for M, N being Subset of the carrier of MS 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,b3let M,
N be
Subset of the
carrier of
MS;
( 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 A19:
(
M is
being_line &
N is
being_line )
and A20:
(
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 )
and
o <> a3
and A21:
o <> b1
and
o <> b2
and A22:
o <> b3
and A23:
a3,
b2 // a2,
b1
and A24:
a3,
b3 // a1,
b1
;
a1,b2 // a2,b3reconsider M9 =
M,
N9 =
N as
Subset of
AffinStruct(# the
carrier of
MS, the
CONGR of
MS #) ;
reconsider a =
a1,
b =
a2,
c =
a3,
a9 =
b1,
b9 =
b2,
c9 =
b3 as
Element of
AffinStruct(# the
carrier of
MS, the
CONGR of
MS #) ;
A25:
c,
c9 // a,
a9
by A24, ANALMETR:36;
a2,
b1 // a3,
b2
by A23, ANALMETR:59;
then A26:
b,
a9 // c,
b9
by ANALMETR:36;
(
M9 is
being_line &
N9 is
being_line )
by A19, ANALMETR:43;
then
b,
c9 // a,
b9
by A18, A20, A21, A22, A26, A25, AFF_2:def 2;
then
a2,
b3 // a1,
b2
by ANALMETR:36;
hence
a1,
b2 // a2,
b3
by ANALMETR:59;
verum end; hence
MS is
satisfying_PAP
by CONMETR:def 2;
verum end;
hence
( MS is satisfying_PAP iff AffinStruct(# the carrier of MS, the CONGR of MS #) is Pappian )
by A1; verum