let S be OAffinPlane; :: thesis: 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 Th51;
hence Lambda S is AffinPlane by Def8, Th48; :: thesis: verum