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