set OAS = the strict OAffinSpace;
A1: ( ( for x, y, z, t being Element of the strict OAffinSpace st x,y // z,t holds
z,t // x,y ) & ( for x, y being Element of the strict OAffinSpace holds x,y // x,y ) ) by DIRAF:1, DIRAF:2;
( ( for x, y, z, t, a, b being Element of the strict OAffinSpace st x,y // a,b & a,b // z,t & a <> b holds
x,y // z,t ) & ( for x, y, z being Element of the strict OAffinSpace holds x,x // y,z ) ) by DIRAF:3, DIRAF:4;
then the strict OAffinSpace is CongrSpace-like by A1;
hence ex b₁ being non empty AffinStruct st
( b₁ is strict & b₁ is CongrSpace-like ) ; :: thesis: verum