for SAS being AffinPlane
for o, a being Element of SAS ex p being Element of SAS st
for b, c being Element of SAS holds
( o,a // o,p & ex d being Element of SAS st
( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) )