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

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