let AFP be AffinPlane; for a, b, o, x, y being Element of AFP st o <> a & o <> b & LIN o,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
( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) )
let a, b, o, x, y be Element of AFP; ( o <> a & o <> b & LIN o,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 ( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) ) )
assume that
A1:
o <> a
and
A2:
o <> b
and
A3:
LIN o,a,b
and
A4:
( ( 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 ) ) )
; ( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) )
A5:
LIN o,b,a
by A3, AFF_1:6;
A6:
now ( LIN o,a,x implies ( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) ) )assume A7:
LIN o,
a,
x
;
( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) )then consider p,
q being
Element of
AFP such that A8:
not
LIN o,
a,
p
and A9:
LIN o,
p,
q
and A10:
a,
p // b,
q
and A11:
p,
x // q,
y
and A12:
LIN o,
a,
y
by A4;
A13:
not
LIN o,
p,
a
by A8, AFF_1:6;
A14:
q,
y // p,
x
by A11, AFF_1:4;
A15:
b,
q // a,
p
by A10, AFF_1:4;
A16:
LIN o,
q,
p
by A9, AFF_1:6;
LIN o,
a,
o
by AFF_1:7;
then A17:
LIN o,
b,
x
by A1, A3, A7, AFF_1:8;
set A =
Line (
o,
b);
A18:
o in Line (
o,
b)
by AFF_1:15;
A19:
a in Line (
o,
b)
by A5, AFF_1:def 2;
A20:
Line (
o,
b) is
being_line
by A2, AFF_1:def 3;
p,
a // q,
b
by A10, AFF_1:4;
then A21:
q <> o
by A2, A3, A13, AFF_1:55;
A22:
not
LIN o,
b,
q
proof
assume
LIN o,
b,
q
;
contradiction
then
q in Line (
o,
b)
by AFF_1:def 2;
then
p in Line (
o,
b)
by A21, A20, A18, A16, AFF_1:25;
hence
contradiction
by A8, A20, A18, A19, AFF_1:21;
verum
end;
y in Line (
o,
b)
by A1, A12, A20, A18, A19, AFF_1:25;
hence
(
o <> b &
o <> a &
LIN o,
b,
a & ( ( not
LIN o,
b,
y &
LIN o,
y,
x &
b,
y // a,
x ) or (
LIN o,
b,
y & ex
p,
p9 being
Element of
AFP st
( not
LIN o,
b,
p &
LIN o,
p,
p9 &
b,
p // a,
p9 &
p,
y // p9,
x &
LIN o,
b,
x ) ) ) )
by A1, A2, A3, A15, A14, A16, A22, A17, AFF_1:6, AFF_1:def 2;
verum end;
now ( not LIN o,a,x implies ( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) ) )assume A23:
not
LIN o,
a,
x
;
( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) )then A24:
not
LIN o,
a,
y
by A1, A2, A3, A4, Lm5;
not
LIN o,
b,
y
proof
A25:
LIN o,
b,
o
by AFF_1:7;
assume A26:
LIN o,
b,
y
;
contradiction
LIN o,
b,
a
by A3, AFF_1:6;
hence
contradiction
by A2, A24, A26, A25, AFF_1:8;
verum
end; hence
(
o <> b &
o <> a &
LIN o,
b,
a & ( ( not
LIN o,
b,
y &
LIN o,
y,
x &
b,
y // a,
x ) or (
LIN o,
b,
y & ex
p,
p9 being
Element of
AFP st
( not
LIN o,
b,
p &
LIN o,
p,
p9 &
b,
p // a,
p9 &
p,
y // p9,
x &
LIN o,
b,
x ) ) ) )
by A1, A2, A3, A4, A23, AFF_1:4, AFF_1:6;
verum end;
hence
( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) )
by A6; verum