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 Th26;
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 by Def5;
a in Line a,b by Th26;
then p,q // a,b by A5, A6, A4, Th36;
hence contradiction by A2, A6, A7, Th46; :: thesis: verum

end;

a <> b by A1, A2, Th47;
then Line a,b is being_line by Def3;
then consider x being Element of AP such that
A8: x in Line a,b and
A9: x in A by A1, A3, Th72;
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