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 ) )
reconsider x9 = x, y9 = y, z9 = z, t9 = t as Element of S by A1;
assume not x,y // z,t ; :: thesis: ex u being Element of AS st
( x,y // x,u & z,t // z,u )
then not x9,y9 '||' z9,t9 by A1, Th45;
then consider u9 being Element of S such that
A2: ( x9,y9 '||' x9,u9 & z9,t9 '||' z9,u9 ) by Th50;
reconsider u = u9 as Element of AS by A1;
( x,y // x,u & z,t // z,u ) by A1, A2, Th45;
hence ex u being Element of AS st
( x,y // x,u & z,t // z,u ) ; :: thesis: verum