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 b1 being non empty AffinStruct st
( b1 is strict & b1 is CongrSpace-like )
; verum