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