let AFP be AffinPlane; for a, b, o, x, y being Element of AFP st o <> a & o <> b & LIN o,a,b & LIN o,a,y & ( ( 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
LIN o,a,x
let a, b, o, x, y be Element of AFP; ( o <> a & o <> b & LIN o,a,b & LIN o,a,y & ( ( 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 LIN o,a,x )
assume that
A1:
o <> a
and
A2:
o <> b
and
A3:
LIN o,a,b
and
A4:
LIN o,a,y
and
A5:
( ( 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 ) ) )
; LIN o,a,x
assume A6:
not LIN o,a,x
; contradiction
then A7:
b <> y
by A2, A3, A5, AFF_1:54;
set A = Line (o,a);
A8:
Line (o,a) is being_line
by A1, AFF_1:def 3;
A9:
b,y // a,x
by A5, A6, AFF_1:4;
A10:
a in Line (o,a)
by AFF_1:15;
A11:
y in Line (o,a)
by A4, AFF_1:def 2;
A12:
o in Line (o,a)
by AFF_1:15;
b in Line (o,a)
by A3, AFF_1:def 2;
then
Line (o,a) = Line (b,y)
by A8, A7, A11, AFF_1:24;
then
x in Line (o,a)
by A7, A10, A9, AFF_1:22;
hence
contradiction
by A6, A8, A12, A10, AFF_1:21; verum