consider S being OAffinPlane;
reconsider AS = Lambda S as AffinSpace by Th48;
for x, y, z, t being Element of AS st not x,y // z,t holds
ex u being Element of AS st
( x,y // x,u & z,t // z,u ) by Th51;
then AS is 2-dimensional by Def8;
hence ex b₁ being AffinSpace st
( b₁ is strict & b₁ is 2-dimensional ) ; :: thesis: verum