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

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

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

a <> b
by A1, A2, Th32;
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;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

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