let AFP be AffinPlane; for o, a, b, x being Element of AFP st o <> a & LIN o,a,b holds
ex y being Element of AFP st
( ( 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 ) ) )
let o, a, b, x be Element of AFP; ( o <> a & LIN o,a,b implies ex y being Element of AFP st
( ( 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 ) ) ) )
assume that
A1:
o <> a
and
A2:
LIN o,a,b
; ex y being Element of AFP st
( ( 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 ) ) )
A3:
now ( LIN o,a,x implies ex y being Element of AFP st
( ( 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 ) ) ) )consider p being
Element of
AFP such that A4:
not
LIN o,
a,
p
by A1, AFF_1:13;
set K =
Line (
o,
p);
o <> p
by A4, AFF_1:7;
then A5:
Line (
o,
p) is
being_line
by AFF_1:def 3;
set A =
Line (
a,
p);
a <> p
by A4, AFF_1:7;
then
Line (
a,
p) is
being_line
by AFF_1:def 3;
then consider B9 being
Subset of
AFP such that A6:
b in B9
and A7:
Line (
a,
p)
// B9
by AFF_1:49;
A8:
B9 is
being_line
by A7, AFF_1:36;
A9:
a in Line (
a,
p)
by AFF_1:15;
A10:
p in Line (
o,
p)
by AFF_1:15;
A11:
p in Line (
a,
p)
by AFF_1:15;
A12:
o in Line (
o,
p)
by AFF_1:15;
not
B9 // Line (
o,
p)
proof
assume
B9 // Line (
o,
p)
;
contradiction
then
Line (
a,
p)
// Line (
o,
p)
by A7, AFF_1:44;
then
Line (
a,
p)
= Line (
o,
p)
by A10, A11, AFF_1:45;
hence
contradiction
by A4, A12, A10, A9, A5, AFF_1:21;
verum
end; then consider p9 being
Element of
AFP such that A13:
p9 in B9
and A14:
p9 in Line (
o,
p)
by A5, A8, AFF_1:58;
A15:
a,
p // b,
p9
by A9, A11, A6, A7, A13, AFF_1:39;
set M =
Line (
o,
a);
A16:
o in Line (
o,
a)
by AFF_1:15;
o <> a
by A4, AFF_1:7;
then A17:
Line (
o,
a) is
being_line
by AFF_1:def 3;
set C =
Line (
p,
x);
assume A18:
LIN o,
a,
x
;
ex y being Element of AFP st
( ( 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 ) ) )then A19:
Line (
p,
x) is
being_line
by A4, AFF_1:def 3;
then consider D being
Subset of
AFP such that A20:
p9 in D
and A21:
Line (
p,
x)
// D
by AFF_1:49;
A22:
p in Line (
p,
x)
by AFF_1:15;
A23:
LIN o,
p,
p9
by A12, A10, A5, A14, AFF_1:21;
A24:
a in Line (
o,
a)
by AFF_1:15;
A25:
x in Line (
p,
x)
by AFF_1:15;
A26:
x in Line (
o,
a)
by A18, AFF_1:def 2;
A27:
not
D // Line (
o,
a)
proof
assume
D // Line (
o,
a)
;
contradiction
then
Line (
p,
x)
// Line (
o,
a)
by A21, AFF_1:44;
then
Line (
p,
x)
= Line (
o,
a)
by A26, A25, AFF_1:45;
hence
contradiction
by A4, A16, A24, A22, A19, AFF_1:21;
verum
end;
D is
being_line
by A21, AFF_1:36;
then consider y being
Element of
AFP such that A28:
y in D
and A29:
y in Line (
o,
a)
by A17, A27, AFF_1:58;
A30:
LIN o,
a,
y
by A16, A24, A17, A29, AFF_1:21;
p,
x // p9,
y
by A22, A25, A20, A21, A28, AFF_1:39;
hence
ex
y being
Element of
AFP st
( ( 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 ) ) )
by A18, A4, A23, A15, A30;
verum end;
now ( not LIN o,a,x implies ex y being Element of AFP st
( ( 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,
a // o,
b
by A2, AFF_1:def 1;
then
a,
o // o,
b
by AFF_1:4;
then consider y being
Element of
AFP such that A31:
x,
o // o,
y
and A32:
x,
a // b,
y
by A1, DIRAF:40;
o,
x // o,
y
by A31, AFF_1:4;
then A33:
LIN o,
x,
y
by AFF_1:def 1;
assume A34:
not
LIN o,
a,
x
;
ex y being Element of AFP st
( ( 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 ) ) )
a,
x // b,
y
by A32, AFF_1:4;
hence
ex
y being
Element of
AFP st
( ( 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 ) ) )
by A34, A33;
verum end;
hence
ex y being Element of AFP st
( ( 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 ) ) )
by A3; verum