consider PAS being Pappian Desarguesian translational Fanoian AffinPlane;
reconsider SAS = PAS as AffinPlane ;
take SAS ; :: thesis: ( ( for o, a, a', b, b', c, c' being Element of SAS st not o,a // o,b & not o,a // o,c & o,a // o,a' & o,b // o,b' & o,c // o,c' & a,b // a',b' & a,c // a',c' holds
b,c // b',c' ) & ( for a, a', b, b', c, c' being Element of SAS st not a,a' // a,b & not a,a' // a,c & a,a' // b,b' & a,a' // c,c' & a,b // a',b' & a,c // a',c' holds
b,c // b',c' ) & ( 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 ) & ( for a, b, c, d being Element of SAS st not a,b // a,c & a,b // c,d & a,c // b,d holds
not a,d // b,c ) )
thus ( ( for o, a, a', b, b', c, c' being Element of SAS st not o,a // o,b & not o,a // o,c & o,a // o,a' & o,b // o,b' & o,c // o,c' & a,b // a',b' & a,c // a',c' holds
b,c // b',c' ) & ( for a, a', b, b', c, c' being Element of SAS st not a,a' // a,b & not a,a' // a,c & a,a' // b,b' & a,a' // c,c' & a,b // a',b' & a,c // a',c' holds
b,c // b',c' ) & ( 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 ) & ( for a, b, c, d being Element of SAS st not a,b // a,c & a,b // c,d & a,c // b,d holds
not a,d // b,c ) ) by Th1, Th2, Th3, PAPDESAF:def 5; :: thesis: verum