set S = the OAffinPlane;
reconsider AS = Lambda the OAffinPlane as AffinSpace by Th41;
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 Th44;
then AS is 2-dimensional ;
hence ex b₁ being AffinSpace st
( b₁ is strict & b₁ is 2-dimensional ) ; :: thesis: verum