let AFP be AffinPlane; for a, b, o, x, y being Element of AFP st o <> a & x = o & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) holds
y = o
let a, b, o, x, y be Element of AFP; ( o <> a & x = o & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) implies y = o )
assume that
A1:
o <> a
and
A2:
x = o
and
A3:
( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) )
; y = o
consider p, p9 being Element of AFP such that
A4:
not LIN o,a,p
and
A5:
LIN o,p,p9
and
a,p // b,p9
and
A6:
p,x // p9,y
and
A7:
LIN o,a,y
by A2, A3, AFF_1:7;
set K = Line (o,p);
A8:
o <> p
by A4, AFF_1:7;
p9 in Line (o,p)
by A5, AFF_1:def 2;
then A9:
y in Line (o,p)
by A2, A6, A8, AFF_1:22;
assume A10:
y <> o
; contradiction
A11:
o in Line (o,p)
by AFF_1:15;
A12:
p in Line (o,p)
by AFF_1:15;
set A = Line (o,a);
A13:
Line (o,a) is being_line
by A1, AFF_1:def 3;
A14:
a in Line (o,a)
by AFF_1:15;
A15:
y in Line (o,a)
by A7, AFF_1:def 2;
A16:
o in Line (o,a)
by AFF_1:15;
Line (o,p) is being_line
by A8, AFF_1:def 3;
then
p in Line (o,a)
by A10, A13, A16, A12, A9, A11, A15, AFF_1:18;
hence
contradiction
by A4, A13, A16, A14, AFF_1:21; verum