let AP be AffinPlane; :: thesis: for a, b being Element of AP
for A being Subset of AP st A is being_line & not a,b // A holds
ex x being Element of AP st
( x in A & LIN a,b,x )
let a, b be Element of AP; :: thesis: for A being Subset of AP st A is being_line & not a,b // A holds
ex x being Element of AP st
( x in A & LIN a,b,x )
let A be Subset of AP; :: thesis: ( A is being_line & not a,b // A implies ex x being Element of AP st
( x in A & LIN a,b,x ) )
assume that
A1: A is being_line and
A2: not a,b // A ; :: thesis: ex x being Element of AP st
( x in A & LIN a,b,x )
set C = Line (a,b);
A3: not Line (a,b) // A

proof

A4: b in Line (a,b) by Th14;
assume Line (a,b) // A ; :: thesis: contradiction
then consider p, q being Element of AP such that
A5: Line (a,b) = Line (p,q) and
A6: p <> q and
A7: p,q // A ;
a in Line (a,b) by Th14;
then p,q // a,b by A5, A6, A4, Th21;
hence contradiction by A2, A6, A7, Th31; :: thesis: verum

end;

a <> b by A1, A2, Th32;
then Line (a,b) is being_line ;
then consider x being Element of AP such that
A8: x in Line (a,b) and
A9: x in A by A1, A3, Th57;
LIN a,b,x by A8, Def2;
hence ex x being Element of AP st
( x in A & LIN a,b,x ) by A9; :: thesis: verum