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