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