let AFP be AffinPlane; for a, b, x, p, p', y, q, q' being Element of
for K being Subset of st a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K & q in K & q' in K & q,a // q',x holds
q,b // q',y
let a, b, x, p, p', y, q, q' be Element of ; for K being Subset of st a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K & q in K & q' in K & q,a // q',x holds
q,b // q',y
let K be Subset of ; ( a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K & q in K & q' in K & q,a // q',x implies q,b // q',y )
assume that
A1:
a,b // K
and
A2:
not a in K
and
A3:
not x in K
and
A4:
AFP is Moufangian
and
A5:
p in K
and
A6:
p' in K
and
A7:
p,a // p',x
and
A8:
p,b // p',y
and
A9:
x,y // K
and
A10:
q in K
and
A11:
q' in K
and
A12:
q,a // q',x
; q,b // q',y
A13:
K is being_line
by A1, AFF_1:40;
A14:
now A15:
a,
q // x,
q'
by A12, AFF_1:13;
A16:
b,
p // y,
p'
by A8, AFF_1:13;
A17:
a,
p // x,
p'
by A7, AFF_1:13;
set A =
Line a,
x;
assume that A18:
not
a,
x // K
and A19:
a <> b
;
q,b // q',y
a <> x
by A13, A18, AFF_1:47;
then A20:
Line a,
x is
being_line
by AFF_1:def 3;
A21:
x in Line a,
x
by AFF_1:26;
A22:
a in Line a,
x
by AFF_1:26;
then consider o being
Element of
such that A23:
o in Line a,
x
and A24:
o in K
by A13, A18, A21, A20, AFF_1:54, AFF_1:72;
A25:
LIN o,
a,
x
by A22, A21, A20, A23, AFF_1:33;
a,
b // x,
y
by A1, A9, AFF_1:40, AFF_1:45;
then
LIN o,
b,
y
by A1, A2, A4, A5, A6, A19, A24, A25, A17, A16, Lm3, AFF_1:40;
then
b,
q // y,
q'
by A1, A2, A4, A9, A10, A11, A13, A24, A25, A15, Lm2;
hence
q,
b // q',
y
by AFF_1:13;
verum end;
A26:
now set M =
Line a,
b;
assume that A27:
a,
x // K
and A28:
a <> b
and A29:
p <> q
;
q,b // q',yA30:
Line a,
b is
being_line
by A28, AFF_1:def 3;
a,
b // a,
x
by A1, A27, AFF_1:40, AFF_1:45;
then
LIN a,
b,
x
by AFF_1:def 1;
then A31:
x in Line a,
b
by AFF_1:def 2;
A32:
b in Line a,
b
by AFF_1:26;
A33:
a in Line a,
b
by AFF_1:26;
A34:
Line a,
b // K
by A1, A28, AFF_1:def 5;
then
x,
y // Line a,
b
by A9, AFF_1:57;
then
y in Line a,
b
by A30, A31, AFF_1:37;
hence
q,
b // q',
y
by A4, A5, A6, A7, A8, A10, A11, A12, A28, A29, A33, A32, A34, A31, Th7;
verum end;
A35:
( a = b implies x = y )
proof
set M =
Line x,
y;
A36:
x in Line x,
y
by AFF_1:26;
assume
a = b
;
x = y
then
p',
x // p',
y
by A2, A5, A7, A8, AFF_1:14;
then
LIN p',
x,
y
by AFF_1:def 1;
then
LIN x,
y,
p'
by AFF_1:15;
then A37:
p' in Line x,
y
by AFF_1:def 2;
assume
x <> y
;
contradiction
then
Line x,
y // K
by A9, AFF_1:def 5;
hence
contradiction
by A3, A6, A36, A37, AFF_1:59;
verum
end;
now assume A38:
p = q
;
q,b // q',y
p' = q'
proof
p',
x // q',
x
by A2, A5, A7, A12, A38, AFF_1:14;
then
x,
p' // x,
q'
by AFF_1:13;
then
LIN x,
p',
q'
by AFF_1:def 1;
then A39:
LIN p',
q',
x
by AFF_1:15;
assume
p' <> q'
;
contradiction
hence
contradiction
by A1, A3, A6, A11, A39, AFF_1:39, AFF_1:40;
verum
end; hence
q,
b // q',
y
by A8, A38;
verum end;
hence
q,b // q',y
by A12, A35, A14, A26; verum