let S be OAffinPlane; Lambda S is AffinPlane
set AS = Lambda S;
for x, y, z, t being Element of (Lambda S) st not x,y // z,t holds
ex u being Element of (Lambda S) st
( x,y // x,u & z,t // z,u )
by Th44;
hence
Lambda S is AffinPlane
by Def7, Th41; verum