let AFP be AffinPlane; for a, b, o, x, y being Element of AFP st o <> a & a = b & ( ( 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
x = y
let a, b, o, x, y be Element of AFP; ( o <> a & a = b & ( ( 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 x = y )
assume that
A1:
o <> a
and
A2:
a = b
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 ) ) )
; x = y
A4:
now ( LIN o,a,x & x <> o implies x = y )A5:
LIN o,
x,
x
by AFF_1:7;
A6:
LIN o,
a,
a
by AFF_1:7;
assume that A7:
LIN o,
a,
x
and A8:
x <> o
;
x = yconsider p,
q being
Element of
AFP such that A9:
not
LIN o,
a,
p
and A10:
LIN o,
p,
q
and A11:
a,
p // b,
q
and A12:
p,
x // q,
y
and A13:
LIN o,
a,
y
by A3, A7;
A14:
LIN o,
p,
p
by AFF_1:7;
A15:
not
LIN o,
p,
x
proof
assume
LIN o,
p,
x
;
contradiction
then A16:
LIN o,
x,
p
by AFF_1:6;
A17:
LIN o,
x,
o
by AFF_1:7;
LIN o,
x,
a
by A7, AFF_1:6;
hence
contradiction
by A8, A9, A17, A16, AFF_1:8;
verum
end;
LIN o,
a,
o
by AFF_1:7;
then A18:
LIN o,
x,
y
by A1, A7, A13, AFF_1:8;
a,
p // a,
p
by AFF_1:2;
then A19:
p,
x // p,
y
by A2, A9, A10, A11, A12, A6, A14, AFF_1:56;
p,
x // p,
x
by AFF_1:2;
hence
x = y
by A14, A15, A18, A19, A5, AFF_1:56;
verum end;
now ( not LIN o,a,x implies x = y )A20:
LIN o,
x,
x
by AFF_1:7;
A21:
LIN o,
a,
a
by AFF_1:7;
A22:
a,
x // a,
x
by AFF_1:2;
assume
not
LIN o,
a,
x
;
x = yhence
x = y
by A2, A3, A22, A21, A20, AFF_1:56;
verum end;
hence
x = y
by A1, A3, A4, Lm7; verum