let AP be AffinPlane; for A, C being Subset of AP st A is being_line & C is being_line & not A // C holds
ex x being Element of AP st
( x in A & x in C )
let A, C be Subset of AP; ( A is being_line & C is being_line & not A // C implies ex x being Element of AP st
( x in A & x in C ) )
assume that
A1:
A is being_line
and
A2:
C is being_line
and
A3:
not A // C
; ex x being Element of AP st
( x in A & x in C )
consider a, b being Element of AP such that
A4:
a <> b
and
A5:
A = Line (a,b)
by A1;
consider c, d being Element of AP such that
A6:
c <> d
and
A7:
C = Line (c,d)
by A2;
not a,b // c,d
by A3, A4, A5, A6, A7, Th36;
then consider x being Element of AP such that
A8:
a,b // a,x
and
A9:
c,d // c,x
by DIRAF:46;
LIN c,d,x
by A9;
then A10:
x in C
by A7, Def2;
LIN a,b,x
by A8;
then
x in A
by A5, Def2;
hence
ex x being Element of AP st
( x in A & x in C )
by A10; verum