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

ex x being Element of AP st

( x in A & x in C )

let A, C be Subset of AP; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum