let AS be non empty AffinStruct ; :: thesis: for S being OAffinPlane st AS = Lambda S holds
for x, y, z, t being Element of st not x,y // z,t holds
ex u being Element of st
( x,y // x,u & z,t // z,u )
let S be OAffinPlane; :: thesis: ( AS = Lambda S implies for x, y, z, t being Element of st not x,y // z,t holds
ex u being Element of st
( x,y // x,u & z,t // z,u ) )
assume A1: AS = Lambda S ; :: thesis: for x, y, z, t being Element of st not x,y // z,t holds
ex u being Element of st
( x,y // x,u & z,t // z,u )
let x, y, z, t be Element of ; :: thesis: ( not x,y // z,t implies ex u being Element of st
( x,y // x,u & z,t // z,u ) )
reconsider x' = x, y' = y, z' = z, t' = t as Element of by A1;
assume not x,y // z,t ; :: thesis: ex u being Element of st
( x,y // x,u & z,t // z,u )
then not x',y' '||' z',t' by A1, Th45;
then consider u' being Element of such that
A2: ( x',y' '||' x',u' & z',t' '||' z',u' ) by Th50;
reconsider u = u' as Element of by A1;
( x,y // x,u & z,t // z,u ) by A1, A2, Th45;
hence ex u being Element of st
( x,y // x,u & z,t // z,u ) ; :: thesis: verum