let AFP be AffinPlane; ( AFP is Moufangian iff for o being Element of AFP
for K being Subset of AFP
for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds
b,c // b9,c9 )
thus
( AFP is Moufangian implies for o being Element of AFP
for K being Subset of AFP
for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds
b,c // b9,c9 )
( ( for o being Element of AFP
for K being Subset of AFP
for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds
b,c // b9,c9 ) implies AFP is Moufangian )proof
assume A1:
AFP is
Moufangian
;
for o being Element of AFP
for K being Subset of AFP
for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds
b,c // b9,c9
let o be
Element of
AFP;
for K being Subset of AFP
for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds
b,c // b9,c9let K be
Subset of
AFP;
for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds
b,c // b9,c9let c,
c9,
a,
b,
a9,
b9 be
Element of
AFP;
( o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 implies b,c // b9,c9 )
assume that A2:
o in K
and A3:
c in K
and A4:
c9 in K
and A5:
K is
being_line
and A6:
LIN o,
a,
a9
and A7:
LIN o,
b,
b9
and A8:
not
a in K
and A9:
a,
b // K
and A10:
a9,
b9 // K
and A11:
a,
c // a9,
c9
;
b,c // b9,c9
A12:
a,
b // a9,
b9
by A5, A9, A10, AFF_1:31;
A13:
now ( o <> c implies b,c // b9,c9 )A14:
now ( a = b implies b,c // b9,c9 )assume A15:
a = b
;
b,c // b9,c9A16:
now ( a9,o // K implies not a9 <> b9 )A17:
not
o,
a // K
by A2, A8, AFF_1:34, AFF_1:35;
A18:
LIN o,
b9,
b
by A7, AFF_1:6;
assume that A19:
a9,
o // K
and A20:
a9 <> b9
;
contradiction
o,
a // o,
a9
by A6, AFF_1:def 1;
then
a9,
o // o,
a
by AFF_1:4;
then A21:
(
o,
a // K or
a9 = o )
by A19, AFF_1:32;
then
b9 in K
by A2, A5, A8, A10, AFF_1:23;
hence
contradiction
by A2, A5, A8, A15, A20, A21, A17, A18, AFF_1:25;
verum end;
LIN o,
a,
o
by AFF_1:7;
then
LIN a9,
b9,
o
by A2, A6, A7, A8, A15, AFF_1:8;
then
a9,
b9 // a9,
o
by AFF_1:def 1;
hence
b,
c // b9,
c9
by A10, A11, A15, A16, AFF_1:32;
verum end; assume
o <> c
;
b,c // b9,c9hence
b,
c // b9,
c9
by A1, A2, A3, A4, A5, A6, A7, A8, A9, A11, A12, A14, AFF_2:def 7;
verum
now ( o = c implies b,c // b9,c9 )assume A22:
o = c
;
b,c // b9,c9then
LIN b,
b9,
c
by A7, AFF_1:6;
then A23:
b,
b9 // b,
c
by AFF_1:def 1;
LIN a,
c,
a9
by A6, A22, AFF_1:6;
then
LIN a,
c,
c9
by A3, A8, A11, AFF_1:9;
then A24:
LIN c,
c9,
a
by AFF_1:6;
then
LIN c9,
b,
b9
by A2, A4, A5, A7, A8, A22, AFF_1:25;
then
LIN b9,
b,
c9
by AFF_1:6;
then
b9,
b // b9,
c9
by AFF_1:def 1;
then A25:
b,
b9 // b9,
c9
by AFF_1:4;
c = c9
by A3, A4, A5, A8, A24, AFF_1:25;
then
(
b = b9 implies
b,
c // b9,
c9 )
by AFF_1:2;
hence
b,
c // b9,
c9
by A23, A25, AFF_1:5;
verum end;
hence
b,
c // b9,
c9
by A13;
verum
end;
assume A26:
for o being Element of AFP
for K being Subset of AFP
for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds
b,c // b9,c9
; AFP is Moufangian
now for K being Subset of AFP
for o, a, b, c, a9, b9, c9 being Element of AFP st K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & a,b // K holds
b,c // b9,c9let K be
Subset of
AFP;
for o, a, b, c, a9, b9, c9 being Element of AFP st K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & a,b // K holds
b,c // b9,c9let o,
a,
b,
c,
a9,
b9,
c9 be
Element of
AFP;
( K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & a,b // K implies b,c // b9,c9 )assume that A27:
K is
being_line
and A28:
o in K
and A29:
c in K
and A30:
c9 in K
and A31:
not
a in K
and
o <> c
and A32:
a <> b
and A33:
LIN o,
a,
a9
and A34:
LIN o,
b,
b9
and A35:
a,
b // a9,
b9
and A36:
a,
c // a9,
c9
and A37:
a,
b // K
;
b,c // b9,c9
a9,
b9 // K
by A32, A35, A37, AFF_1:32;
hence
b,
c // b9,
c9
by A26, A27, A28, A29, A30, A31, A33, A34, A36, A37;
verum end;
hence
AFP is Moufangian
by AFF_2:def 7; verum