let SAS be AffinPlane; :: thesis: ( SAS is Pappian implies for a1, a2, a3, b1, b2, b3 being Element of SAS st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds
a3,b1 // a1,b3 )
assume A1: SAS is Pappian ; :: thesis: for a1, a2, a3, b1, b2, b3 being Element of SAS st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds
a3,b1 // a1,b3
let a1, a2, a3, b1, b2, b3 be Element of SAS; :: thesis: ( a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 implies a3,b1 // a1,b3 )
assume that
A2: a1,a2 // a1,a3 and
A3: b1,b2 // b1,b3 and
A4: a1,b2 // a2,b1 and
A5: a2,b3 // a3,b2 ; :: thesis: a3,b1 // a1,b3
LIN a1,a2,a3 by A2, AFF_1:def 1;
then consider M being Subset of SAS such that
A6: M is being_line and
A7: a1 in M and
A8: a2 in M and
A9: a3 in M by AFF_1:21;
LIN b1,b2,b3 by A3, AFF_1:def 1;
then consider N being Subset of SAS such that
A10: N is being_line and
A11: b1 in N and
A12: b2 in N and
A13: b3 in N by AFF_1:21;

A14: now :: thesis: ( M <> N & not M // N implies a3,b1 // a1,b3 )

assume that
A15: M <> N and
A16: not M // N ; :: thesis: a3,b1 // a1,b3
consider o being Element of SAS such that
A17: o in M and
A18: o in N by A6, A10, A16, AFF_1:58;

A19: now :: thesis: ( o <> a1 & b1 <> o & o = b3 implies a3,b1 // a1,b3 )

assume that
A20: o <> a1 and
A21: b1 <> o and
A22: o = b3 ; :: thesis: a3,b1 // a1,b3

A23: now :: thesis: ( a2 <> o implies a3,b1 // a1,b3 )

assume a2 <> o ; :: thesis: a3,b1 // a1,b3
then b2 in M by A5, A6, A8, A9, A17, A22, AFF_1:48;
then b2 = o by A6, A10, A12, A15, A17, A18, AFF_1:18;
then b1 in M by A4, A6, A7, A8, A17, A20, AFF_1:48;
hence a3,b1 // a1,b3 by A6, A7, A9, A17, A22, AFF_1:51; :: thesis: verum

end;

now :: thesis: ( a2 = o implies a3,b1 // a1,b3 )

assume a2 = o ; :: thesis: a3,b1 // a1,b3
then o,b1 // b2,a1 by A4, AFF_1:4;
then a1 in N by A10, A11, A12, A13, A21, A22, AFF_1:48;
hence a3,b1 // a1,b3 by A6, A7, A10, A15, A17, A18, A20, AFF_1:18; :: thesis: verum

end;

hence a3,b1 // a1,b3 by A23; :: thesis: verum

end;

A24: now :: thesis: ( o <> a1 & b1 = o implies a3,b1 // a1,b3 )

assume that
o <> a1 and
A25: b1 = o ; :: thesis: a3,b1 // a1,b3
A26: o,a2 // a1,b2 by A4, A25, AFF_1:4;

A27: now :: thesis: ( a2 <> o implies a3,b1 // a1,b3 )

assume a2 <> o ; :: thesis: a3,b1 // a1,b3
then b2 in M by A6, A7, A8, A17, A26, AFF_1:48;
then b2 = o by A6, A10, A12, A15, A17, A18, AFF_1:18;
then A28: o,a3 // a2,b3 by A5, AFF_1:4;

now :: thesis: ( o <> a3 implies a3,b1 // a1,b3 )

assume o <> a3 ; :: thesis: a3,b1 // a1,b3
then b3 in M by A6, A8, A9, A17, A28, AFF_1:48;
hence a3,b1 // a1,b3 by A6, A7, A9, A17, A25, AFF_1:51; :: thesis: verum

end;

hence a3,b1 // a1,b3 by A25, AFF_1:3; :: thesis: verum

end;

now :: thesis: ( a2 = o implies a3,b1 // a1,b3 )

assume A29: a2 = o ; :: thesis: a3,b1 // a1,b3

now :: thesis: ( b3 <> o implies a3,b1 // a1,b3 )

assume A30: b3 <> o ; :: thesis: a3,b1 // a1,b3
o,b3 // b2,a3 by A5, A29, AFF_1:4;
then a3 in N by A10, A12, A13, A18, A30, AFF_1:48;
then b1 = a3 by A6, A9, A10, A15, A17, A18, A25, AFF_1:18;
hence a3,b1 // a1,b3 by AFF_1:3; :: thesis: verum

end;

hence a3,b1 // a1,b3 by A6, A7, A9, A17, A25, AFF_1:51; :: thesis: verum

end;

hence a3,b1 // a1,b3 by A27; :: thesis: verum

end;

A31: now :: thesis: ( o = a1 implies a3,b1 // a1,b3 )

assume A32: o = a1 ; :: thesis: a3,b1 // a1,b3
then A33: o,b2 // b1,a2 by A4, AFF_1:4;

A34: now :: thesis: ( b2 <> o implies a3,b1 // a1,b3 )

assume b2 <> o ; :: thesis: a3,b1 // a1,b3
then a2 in N by A10, A11, A12, A18, A33, AFF_1:48;
then a2 = o by A6, A8, A10, A15, A17, A18, AFF_1:18;
then A35: o,b3 // b2,a3 by A5, AFF_1:4;

now :: thesis: ( o <> b3 implies a3,b1 // a1,b3 )

assume o <> b3 ; :: thesis: a3,b1 // a1,b3
then a3 in N by A10, A12, A13, A18, A35, AFF_1:48;
hence a3,b1 // a1,b3 by A10, A11, A13, A18, A32, AFF_1:51; :: thesis: verum

end;

hence a3,b1 // a1,b3 by A32, AFF_1:3; :: thesis: verum

end;

now :: thesis: ( b2 = o implies a3,b1 // a1,b3 )

assume A36: b2 = o ; :: thesis: a3,b1 // a1,b3

now :: thesis: ( a3 <> o implies a3,b1 // a1,b3 )

assume A37: a3 <> o ; :: thesis: a3,b1 // a1,b3
o,a3 // a2,b3 by A5, A36, AFF_1:4;
then b3 in M by A6, A8, A9, A17, A37, AFF_1:48;
then a1 = b3 by A6, A10, A13, A15, A17, A18, A32, AFF_1:18;
hence a3,b1 // a1,b3 by AFF_1:3; :: thesis: verum

end;

hence a3,b1 // a1,b3 by A10, A11, A13, A18, A32, AFF_1:51; :: thesis: verum

end;

hence a3,b1 // a1,b3 by A34; :: thesis: verum

end;

A38: now :: thesis: ( o <> a1 & b1 <> o & o <> b3 & o = a3 implies a3,b1 // a1,b3 )

assume that
A39: o <> a1 and
A40: b1 <> o and
o <> b3 and
A41: o = a3 ; :: thesis: a3,b1 // a1,b3
A42: o,b2 // b3,a2 by A5, A41, AFF_1:4;

A43: now :: thesis: ( b2 <> o implies a3,b1 // a1,b3 )

assume b2 <> o ; :: thesis: a3,b1 // a1,b3
then a2 in N by A10, A12, A13, A18, A42, AFF_1:48;
then a2 = o by A6, A8, A10, A15, A17, A18, AFF_1:18;
then o,b1 // b2,a1 by A4, AFF_1:4;
then a1 in N by A10, A11, A12, A18, A40, AFF_1:48;
hence a3,b1 // a1,b3 by A10, A11, A13, A18, A41, AFF_1:51; :: thesis: verum

end;

now :: thesis: ( b2 = o implies a3,b1 // a1,b3 )

assume b2 = o ; :: thesis: a3,b1 // a1,b3
then b1 in M by A4, A6, A7, A8, A9, A39, A41, AFF_1:48;
hence a3,b1 // a1,b3 by A6, A10, A11, A15, A17, A18, A40, AFF_1:18; :: thesis: verum

end;

hence a3,b1 // a1,b3 by A43; :: thesis: verum

end;

now :: thesis: ( o <> a1 & o <> b1 & o <> b3 & o <> a3 implies a3,b1 // a1,b3 )

assume that
A44: ( o <> a1 & o <> b1 ) and
A45: o <> b3 and
A46: o <> a3 ; :: thesis: a3,b1 // a1,b3
A47: o <> b2

proof

assume o = b2 ; :: thesis: contradiction
then o,a3 // a2,b3 by A5, AFF_1:4;
then b3 in M by A6, A8, A9, A17, A46, AFF_1:48;
hence contradiction by A6, A10, A13, A15, A17, A18, A45, AFF_1:18; :: thesis: verum

end;

o <> a2

proof

assume o = a2 ; :: thesis: contradiction
then o,b3 // b2,a3 by A5, AFF_1:4;
then a3 in N by A10, A12, A13, A18, A45, AFF_1:48;
hence contradiction by A6, A9, A10, A15, A17, A18, A46, AFF_1:18; :: thesis: verum

end;

then a1,b3 // a3,b1 by A1, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A15, A17, A18, A44, A45, A46, A47, AFF_2:def 2;
hence a3,b1 // a1,b3 by AFF_1:4; :: thesis: verum

end;

hence a3,b1 // a1,b3 by A31, A24, A19, A38; :: thesis: verum

end;

A48: SAS is satisfying_pap by A1, AFF_2:9;

now :: thesis: ( M <> N & M // N implies a3,b1 // a1,b3 )

assume ( M <> N & M // N ) ; :: thesis: a3,b1 // a1,b3
then a1,b3 // a3,b1 by A48, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, AFF_2:def 13;
hence a3,b1 // a1,b3 by AFF_1:4; :: thesis: verum

end;

hence a3,b1 // a1,b3 by A6, A7, A9, A11, A13, A14, AFF_1:51; :: thesis: verum