let AP be AffinPlane; 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; ( 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
; 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; verum