let AP be AffinPlane; :: thesis: ( AP is Pappian iff AP is satisfying_PAP_1 )
A1: now
assume A2: AP is satisfying_PAP_1 ; :: thesis: AP is Pappian
thus AP is Pappian :: thesis: verum
proof
let M be Subset of ; :: according to AFF_2:def 2 :: thesis: for N being Subset of
for o, a, b, c, a', b', c' being Element of 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 N be Subset of ; :: thesis: for o, a, b, c, a', b', c' being Element of 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 ; :: 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 and
A4: N is being_line and
A5: ( M <> N & o in M & o in N ) and
A6: o <> a and
A7: o <> a' and
A8: o <> b and
A9: o <> b' and
A10: ( o <> c & o <> c' ) and
A11: a in M and
A12: b in M and
A13: c in M and
A14: a' in N and
A15: b' in N and
A16: c' in N and
A17: a,b' // b,a' and
A18: b,c' // c,b' ; :: thesis: a,c' // c,a'
set A = Line a,c';
set P = Line b,a';
A19: b <> a' by A3, A4, A5, A7, A12, A14, AFF_1:30;
then A20: b in Line b,a' by AFF_1:38;
assume A21: not a,c' // c,a' ; :: thesis: contradiction
then A22: a <> c' by AFF_1:12;
then A23: ( a in Line a,c' & c' in Line a,c' ) by AFF_1:38;
A24: a' in Line b,a' by A19, AFF_1:38;
Line a,c' is being_line by A22, AFF_1:38;
then consider K being Subset of such that
A25: c in K and
A26: Line a,c' // K by AFF_1:63;
A27: b <> c
proof
assume A28: b = c ; :: thesis: contradiction
then LIN b,c',b' by A18, AFF_1:def 1;
then LIN b',c',b by AFF_1:15;
then ( b' = c' or b in N ) by A4, A15, A16, AFF_1:39;
hence contradiction by A3, A4, A5, A8, A12, A17, A21, A28, AFF_1:30; :: thesis: verum
end;
A29: b' <> c'
proof
assume b' = c' ; :: thesis: contradiction
then b',b // b',c by A18, AFF_1:13;
then LIN b',b,c by AFF_1:def 1;
then LIN b,c,b' by AFF_1:15;
then b' in M by A3, A12, A13, A27, AFF_1:39;
hence contradiction by A3, A4, A5, A9, A15, AFF_1:30; :: thesis: verum
end;
A30: not Line b,a' // K
proof
assume Line b,a' // K ; :: thesis: contradiction
then Line b,a' // Line a,c' by A26, AFF_1:58;
then b,a' // a,c' by A23, A20, A24, AFF_1:53;
then a,b' // a,c' by A17, A19, AFF_1:14;
then LIN a,b',c' by AFF_1:def 1;
then LIN b',c',a by AFF_1:15;
then a in N by A4, A15, A16, A29, AFF_1:39;
hence contradiction by A3, A4, A5, A6, A11, AFF_1:30; :: thesis: verum
end;
A31: Line b,a' is being_line by A19, AFF_1:38;
K is being_line by A26, AFF_1:50;
then consider x being Element of such that
A32: x in Line b,a' and
A33: x in K by A31, A30, AFF_1:72;
A34: a,c' // c,x by A23, A25, A26, A33, AFF_1:53;
LIN b,x,a' by A31, A20, A24, A32, AFF_1:33;
then b,x // b,a' by AFF_1:def 1;
then a,b' // b,x by A17, A19, AFF_1:14;
then x in N by A2, A3, A4, A5, A6, A8, A9, A10, A11, A12, A13, A15, A16, A18, A27, A34, Def3;
then N = Line b,a' by A4, A14, A21, A31, A24, A32, A34, AFF_1:30;
hence contradiction by A3, A4, A5, A8, A12, A20, AFF_1:30; :: thesis: verum
end;
end;
now
assume A35: AP is Pappian ; :: thesis: AP is satisfying_PAP_1
thus AP is satisfying_PAP_1 :: thesis: verum
proof
let M be Subset of ; :: according to AFF_2:def 3 :: thesis: for N being Subset of
for o, a, b, c, a', b', c' being Element of 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 & b' in N & c' in N & a,b' // b,a' & b,c' // c,b' & a,c' // c,a' & b <> c holds
a' in N
let N be Subset of ; :: thesis: for o, a, b, c, a', b', c' being Element of 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 & b' in N & c' in N & a,b' // b,a' & b,c' // c,b' & a,c' // c,a' & b <> c holds
a' in N
let o, a, b, c, a', b', c' be Element of ; :: 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 & b' in N & c' in N & a,b' // b,a' & b,c' // c,b' & a,c' // c,a' & b <> c implies a' in N )
assume that
A36: M is being_line and
A37: N is being_line and
A38: M <> N and
A39: o in M and
A40: o in N and
A41: o <> a and
o <> a' and
A42: o <> b and
A43: o <> b' and
A44: o <> c and
A45: o <> c' and
A46: a in M and
A47: b in M and
A48: c in M and
A49: b' in N and
A50: c' in N and
A51: a,b' // b,a' and
A52: b,c' // c,b' and
A53: a,c' // c,a' and
A54: b <> c ; :: thesis: a' in N
A55: a <> c' by A36, A37, A38, A39, A40, A41, A46, A50, AFF_1:30;
A56: b <> a' not b,a' // N then consider x being Element of such that
A58: x in N and
A59: LIN b,a',x by A37, AFF_1:73;
A60: b,a' // b,x by A59, AFF_1:def 1;
A61: o <> x a,b' // b,x by A51, A56, A60, AFF_1:14;
then a,c' // c,x by A35, A36, A37, A38, A39, A40, A41, A42, A43, A44, A45, A46, A47, A48, A49, A50, A52, A58, A61, Def2;
then c,a' // c,x by A53, A55, AFF_1:14;
then LIN c,a',x by AFF_1:def 1;
then A62: LIN a',x,c by AFF_1:15;
A63: LIN a',x,x by AFF_1:16;
assume A64: not a' in N ; :: thesis: contradiction
LIN a',x,b by A59, AFF_1:15;
then x in M by A36, A47, A48, A54, A64, A58, A62, A63, AFF_1:17, AFF_1:39;
hence contradiction by A36, A37, A38, A39, A40, A58, A61, AFF_1:30; :: thesis: verum
end;
end;
hence ( AP is Pappian iff AP is satisfying_PAP_1 ) by A1; :: thesis: verum