let AP be AffinPlane; :: thesis: for a, b, c, d being Element of st not a,b // c,d holds
ex p being Element of st
( LIN a,b,p & LIN c,d,p )
let a, b, c, d be Element of ; :: thesis: ( not a,b // c,d implies ex p being Element of st
( LIN a,b,p & LIN c,d,p ) )
assume not a,b // c,d ; :: thesis: ex p being Element of st
( LIN a,b,p & LIN c,d,p )
then consider p being Element of such that
A1: a,b // a,p and
A2: c,d // c,p by DIRAF:54;
A3: LIN c,d,p by A2, Def1;
LIN a,b,p by A1, Def1;
hence ex p being Element of st
( LIN a,b,p & LIN c,d,p ) by A3; :: thesis: verum