let AP be AffinPlane; :: thesis: ( AP is satisfying_PPAP iff ( AP is Pappian & AP is satisfying_pap ) )
A1: ( AP is Pappian & AP is satisfying_pap implies AP is satisfying_PPAP )
proof
assume that
A2: AP is Pappian and
A3: AP is satisfying_pap ; :: thesis: AP is satisfying_PPAP
thus AP is satisfying_PPAP :: thesis: verum
proof
let M be Subset of AP; :: according to AFF_2:def 1 :: thesis: for N being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & 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,a9
let N be Subset of AP; :: thesis: for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & 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,a9
let a, b, c, a9, b9, c9 be Element of AP; :: thesis: ( M is being_line & N is being_line & 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
A4: M is being_line and
A5: N is being_line and
A6: a in M and
A7: b in M and
A8: c in M and
A9: a9 in N and
A10: b9 in N and
A11: c9 in N and
A12: a,b9 // b,a9 and
A13: b,c9 // c,b9 ; :: thesis: a,c9 // c,a9
now :: thesis: ( M <> N & not a,c9 // c,a9 implies a,c9 // c,a9 )
assume A14: M <> N ; :: thesis: ( not a,c9 // c,a9 implies a,c9 // c,a9 )
assume A15: not a,c9 // c,a9 ; :: thesis: a,c9 // c,a9
now :: thesis: ( not M // N implies a,c9 // c,a9 )
assume not M // N ; :: thesis: a,c9 // c,a9
then consider o being Element of AP such that
A16: o in M and
A17: o in N by A4, A5, AFF_1:58;
A18: o <> a
proof
assume A19: o = a ; :: thesis: contradiction
then o,b9 // a9,b by A12, AFF_1:4;
then ( o = b9 or b in N ) by A5, A9, A10, A17, AFF_1:48;
then ( o = b9 or o = b ) by A4, A5, A7, A14, A16, A17, AFF_1:18;
then ( c,o // b,c9 or o,c9 // b9,c ) by A13, AFF_1:4;
then ( c9 in M or c = o or c in N or o = c9 ) by A4, A5, A7, A8, A10, A11, A16, A17, AFF_1:48;
then ( o = c or o = c9 ) by A4, A5, A8, A11, A14, A16, A17, AFF_1:18;
hence contradiction by A5, A9, A11, A15, A17, A19, AFF_1:3, AFF_1:51; :: thesis: verum
end;
A20: o <> b
proof
assume A21: o = b ; :: thesis: contradiction
then o,c9 // b9,c by A13, AFF_1:4;
then ( o = c9 or c in N ) by A5, A10, A11, A17, AFF_1:48;
then A22: ( o = c9 or o = c ) by A4, A5, A8, A14, A16, A17, AFF_1:18;
o,a9 // b9,a by A12, A21, AFF_1:4;
then ( o = a9 or a in N ) by A5, A9, A10, A17, AFF_1:48;
hence contradiction by A4, A5, A6, A8, A14, A15, A16, A17, A18, A22, AFF_1:3, AFF_1:18, AFF_1:51; :: thesis: verum
end;
A23: o <> c9
proof
assume A24: o = c9 ; :: thesis: contradiction
then b9 in M by A4, A7, A8, A13, A16, A20, AFF_1:48;
then a,o // b,a9 by A4, A5, A10, A12, A14, A16, A17, AFF_1:18;
then a9 in M by A4, A6, A7, A16, A18, AFF_1:48;
hence contradiction by A4, A6, A8, A15, A16, A24, AFF_1:51; :: thesis: verum
end;
A25: o <> c
proof
assume A26: o = c ; :: thesis: contradiction
then o,b9 // c9,b by A13, AFF_1:4;
then ( o = b9 or b in N ) by A5, A10, A11, A17, AFF_1:48;
then a9 in M by A4, A5, A6, A7, A9, A12, A16, A17, A18, A20, AFF_1:18, AFF_1:48;
then a9 = o by A4, A5, A9, A14, A16, A17, AFF_1:18;
hence contradiction by A15, A26, AFF_1:3; :: thesis: verum
end;
A27: o <> a9 o <> b9 hence a,c9 // c,a9 by A2, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A16, A17, A18, A20, A25, A27, A23; :: thesis: verum
end;
hence a,c9 // c,a9 by A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14; :: thesis: verum
end;
hence a,c9 // c,a9 by A4, A6, A8, A9, A11, AFF_1:51; :: thesis: verum
end;
end;
thus ( AP is satisfying_PPAP iff ( AP is Pappian & AP is satisfying_pap ) ) by A1; :: thesis: verum