let MS be OrtAfPl; :: thesis: ( MS is satisfying_PAP iff Af MS is Pappian )
set AS = Af MS;
A1:
now assume A2:
MS is
satisfying_PAP
;
:: thesis: Af MS is Pappian now let M,
N be
Subset of
(Af MS);
:: thesis: for o, a, b, c, a', b', c' being Element of the carrier of (Af MS) st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a' & o <> b & o <> b' & o <> c & o <> c' & a in M & b in M & c in M & a' in N & b' in N & c' in N & a,b' // b,a' & b,c' // c,b' holds
a,c' // c,a'let o,
a,
b,
c,
a',
b',
c' be
Element of the
carrier of
(Af MS);
:: thesis: ( M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a' & o <> b & o <> b' & o <> c & o <> c' & a in M & b in M & c in M & a' in N & b' in N & c' in N & a,b' // b,a' & b,c' // c,b' implies a,c' // c,a' )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 &
o <> a' &
o <> b &
o <> b' &
o <> c &
o <> c' )
and A7:
(
a in M &
b in M &
c in M &
a' in N &
b' in N &
c' in N )
and A8:
(
a,
b' // b,
a' &
b,
c' // c,
b' )
;
:: thesis: a,c' // c,a'reconsider M' =
M,
N' =
N as
Subset of
MS by ANALMETR:57;
A9:
(
M' is
being_line &
N' is
being_line )
by A3, ANALMETR:58;
reconsider a1 =
a,
b1 =
b,
c1 =
c,
a1' =
a',
b1' =
b',
c1' =
c' as
Element of the
carrier of
MS by ANALMETR:47;
A10:
( not
a1' in M' & not
b1 in N' )
by A4, A5, A6, A7, A9, CONMETR:5;
(
a1,
b1' // b1,
a1' &
b1,
c1' // c1,
b1' )
by A8, ANALMETR:48;
then
(
b1,
a1' // a1,
b1' &
b1,
c1' // c1,
b1' )
by ANALMETR:81;
then
c1,
a1' // a1,
c1'
by A2, A5, A6, A7, A9, A10, CONMETR:def 2;
then
a1,
c1' // c1,
a1'
by ANALMETR:81;
hence
a,
c' // c,
a'
by ANALMETR:48;
:: thesis: verum end; hence
Af MS is
Pappian
by AFF_2:def 2;
:: thesis: verum end;
now assume A11:
Af MS is
Pappian
;
:: thesis: MS is satisfying_PAP now let o,
a1,
a2,
a3,
b1,
b2,
b3 be
Element of
MS;
:: thesis: 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;
:: 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 A12:
(
M is
being_line &
N is
being_line )
and A13:
(
o in M &
a1 in M &
a2 in M &
a3 in M &
o in N &
b1 in N &
b2 in N &
b3 in N )
and A14:
( not
b2 in M & not
a3 in N )
and A15:
(
o <> a1 &
o <> a2 &
o <> a3 &
o <> b1 &
o <> b2 &
o <> b3 )
and A16:
(
a3,
b2 // a2,
b1 &
a3,
b3 // a1,
b1 )
;
:: thesis: a1,b2 // a2,b3A17:
(
a2,
b1 // a3,
b2 &
a3,
b3 // a1,
b1 )
by A16, ANALMETR:81;
reconsider M' =
M,
N' =
N as
Subset of
(Af MS) by ANALMETR:57;
A18:
(
M' is
being_line &
N' is
being_line )
by A12, ANALMETR:58;
reconsider a =
a1,
b =
a2,
c =
a3,
a' =
b1,
b' =
b2,
c' =
b3 as
Element of the
carrier of
(Af MS) by ANALMETR:47;
(
b,
a' // c,
b' &
c,
c' // a,
a' )
by A17, ANALMETR:48;
then
b,
c' // a,
b'
by A11, A13, A14, A15, A18, AFF_2:def 2;
then
a2,
b3 // a1,
b2
by ANALMETR:48;
hence
a1,
b2 // a2,
b3
by ANALMETR:81;
:: thesis: verum end; hence
MS is
satisfying_PAP
by CONMETR:def 2;
:: thesis: verum end;
hence
( MS is satisfying_PAP iff Af MS is Pappian )
by A1; :: thesis: verum