consider OAS being strict OAffinSpace;
A1: ( ( for x, y, z, t being Element of OAS st x,y // z,t holds
z,t // x,y ) & ( for x, y being Element of OAS holds x,y // x,y ) ) by DIRAF:4, DIRAF:5;
( ( for x, y, z, t, a, b being Element of OAS st x,y // a,b & a,b // z,t & a <> b holds
x,y // z,t ) & ( for x, y, z being Element of OAS holds x,x // y,z ) ) by DIRAF:6, DIRAF:7;
then OAS is CongrSpace-like by A1, Def5;
hence ex b₁ being non empty AffinStruct st
( b₁ is strict & b₁ is CongrSpace-like ) ; :: thesis: verum