let X be OrtAfPl; :: thesis:
assume that
A1: X is satisfying_OPAP and
A2: X is satisfying_DES ; :: thesis:
let o be Element of X; :: according to CONMETR:def 2 :: thesis:
let a1, a2, a3, b1, b2, b3 be Element of X; :: thesis:
let M, N be Subset of X; :: thesis:
assume that
A3: ( M is being_line & N is being_line ) and
A4: ( o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 ) ; :: thesis:
reconsider o' = o, a1' = a1, a2' = a2, a3' = a3, b1' = b1, b2' = b2, b3' = b3 as Element of (Af X) by ANALMETR:47;
reconsider M' = M, N' = N as Subset of (Af X) by ANALMETR:57;
A5: ( M' is being_line & N' is being_line ) by A3, ANALMETR:58;
then A6: ( M' // M' & N' // N' ) by AFF_1:55;

now

assume A7: not M _|_ N ; :: thesis:

A8: now

assume A9: a1 = a2 ; :: thesis:
A10: not LIN o',a3',b2' by A4, A5, AFF_1:39;
A11: LIN o',b2',b3'

proof

o',b2' // o',b3' by A4, A6, AFF_1:53;
hence LIN o',b2',b3' by AFF_1:def 1; :: thesis:

end;

a3',b2' // a3',b3'

proof

a1 <> b1

proof

assume A12: a1 = b1 ; :: thesis:
o',a1' // o',a3' by A4, A6, AFF_1:53;
then LIN o',a1',a3' by AFF_1:def 1;
hence contradiction by A4, A5, A12, AFF_1:39; :: thesis:

end;

then a3,b2 // a3,b3 by A4, A9, ANALMETR:82;
hence a3',b2' // a3',b3' by ANALMETR:48; :: thesis:

end;

then b2' = b3' by A10, A11, AFF_1:23;
then a1',b2' // a2',b3' by A9, AFF_1:11;
hence a1,b2 // a2,b3 by ANALMETR:48; :: thesis:

end;

A13: now

assume A14: a2 = a3 ; :: thesis:
A15: not LIN o',a3',b2' by A4, A5, AFF_1:39;
A16: LIN o',b2',b1'

proof

o',b2' // o',b1' by A4, A6, AFF_1:53;
hence LIN o',b2',b1' by AFF_1:def 1; :: thesis:

end;

a3',b2' // a3',b1' by A4, A14, ANALMETR:48;
then b2' = b1' by A15, A16, AFF_1:23;
hence a1,b2 // a2,b3 by A4, A14, ANALMETR:81; :: thesis:

end;

A17: now

assume A18: a1 = a3 ; :: thesis:
A19: not LIN o',a3',b3'

proof

assume LIN o',a3',b3' ; :: thesis:
then LIN o',b3',a3' by AFF_1:15;
hence contradiction by A4, A5, AFF_1:39; :: thesis:

end;

A20: LIN o',b3',b1'

proof

o',b3' // o',b1' by A4, A6, AFF_1:53;
hence LIN o',b3',b1' by AFF_1:def 1; :: thesis:

end;

a3',b3' // a3',b1' by A4, A18, ANALMETR:48;
hence a1,b2 // a2,b3 by A4, A18, A19, A20, AFF_1:23; :: thesis:

end;

now

assume A21: ( a1 <> a2 & a2 <> a3 & a1 <> a3 ) ; :: thesis:
A22: ( b1 <> b2 & b2 <> b3 & b1 <> b3 )

proof

assume A23: ( b1 = b2 or b2 = b3 or b1 = b3 ) ; :: thesis:

A24: now

assume A25: b1 = b2 ; :: thesis:
A26: not LIN o',b2',a2'

proof

assume LIN o',b2',a2' ; :: thesis:
then LIN o',a2',b2' by AFF_1:15;
hence contradiction by A4, A5, AFF_1:39; :: thesis:

end;

A27: LIN o',a2',a3'

proof

o',a2' // o',a3' by A4, A6, AFF_1:53;
hence LIN o',a2',a3' by AFF_1:def 1; :: thesis:

end;

b2',a2' // b2',a3'

proof

b2,a2 // b2,a3 by A4, A25, ANALMETR:81;
hence b2',a2' // b2',a3' by ANALMETR:48; :: thesis:

end;

hence contradiction by A21, A26, A27, AFF_1:23; :: thesis:

end;

A28: now

assume A29: b2 = b3 ; :: thesis:
A30: not LIN o',b1',a1'

proof

assume LIN o',b1',a1' ; :: thesis:
then A31: a1' in N' by A4, A5, AFF_1:39;
o',a1' // o',a3' by A4, A6, AFF_1:53;
then LIN o',a1',a3' by AFF_1:def 1;
hence contradiction by A4, A5, A31, AFF_1:39; :: thesis:

end;

A32: LIN o',a1',a2'

proof

o',a1' // o',a2' by A4, A6, AFF_1:53;
hence LIN o',a1',a2' by AFF_1:def 1; :: thesis:

end;

b1',a1' // b1',a2'

proof

a1,b1 // a2,b1 by A4, A29, ANALMETR:82;
then b1,a1 // b1,a2 by ANALMETR:81;
hence b1',a1' // b1',a2' by ANALMETR:48; :: thesis:

end;

hence contradiction by A21, A30, A32, AFF_1:23; :: thesis:

end;

now

assume A33: b1 = b3 ; :: thesis:
A34: not LIN o',b1',a1'

proof

assume LIN o',b1',a1' ; :: thesis:
then A35: a1' in N' by A4, A5, AFF_1:39;
o',a1' // o',a3' by A4, A6, AFF_1:53;
then LIN o',a1',a3' by AFF_1:def 1;
hence contradiction by A4, A5, A35, AFF_1:39; :: thesis:

end;

A36: LIN o',a1',a3'

proof

o',a1' // o',a3' by A4, A6, AFF_1:53;
hence LIN o',a1',a3' by AFF_1:def 1; :: thesis:

end;

b1',a1' // b1',a3'

proof

b1,a1 // b1,a3 by A4, A33, ANALMETR:81;
hence b1',a1' // b1',a3' by ANALMETR:48; :: thesis:

end;

hence contradiction by A21, A34, A36, AFF_1:23; :: thesis:

end;

hence contradiction by A23, A24, A28; :: thesis:

end;

A37: now

assume A38: a3,b3 _|_ o,b2 ; :: thesis:
consider x being Element of X such that
A39: ( o,b2 _|_ o,x & o <> x ) by ANALMETR:51;
reconsider x' = x as Element of (Af X) by ANALMETR:47;
LIN o',x',x' by AFF_1:16;
then consider A' being Subset of (Af X) such that
A40: ( A' is being_line & o' in A' & x' in A' & x' in A' ) by AFF_1:33;
reconsider A = A' as Subset of X by ANALMETR:57;
A41: A _|_ N

proof

A42: A = Line o,x

proof

A43: for e1 being Element of X st e1 in A holds
LIN o,x,e1

proof

let e1 be Element of X; :: thesis:
assume A44: e1 in A ; :: thesis:
reconsider e1' = e1 as Element of (Af X) by ANALMETR:47;
A' // A' by A40, AFF_1:55;
then o',x' // o',e1' by A40, A44, AFF_1:53;
then LIN o',x',e1' by AFF_1:def 1;
hence LIN o,x,e1 by ANALMETR:55; :: thesis:

end;

for e1 being Element of X st LIN o,x,e1 holds
e1 in A

proof

let e1 be Element of X; :: thesis:
assume A45: LIN o,x,e1 ; :: thesis:
reconsider e1' = e1 as Element of (Af X) by ANALMETR:47;
LIN o',x',e1' by A45, ANALMETR:55;
hence e1 in A by A39, A40, AFF_1:39; :: thesis:

end;

hence A = Line o,x by A43, ANALMETR:def 12; :: thesis:

end;

o,x _|_ N by A3, A4, A39, ANALMETR:77;
hence A _|_ N by A39, A42, ANALMETR:def 15; :: thesis:

end;

consider e1' being Element of (Af X) such that
A46: ( a3',b2' // b3',e1' & b3' <> e1' ) by DIRAF:47;
not b3',e1' // A'

proof

assume A47: b3',e1' // A' ; :: thesis:
consider d1', d2' being Element of (Af X) such that
A48: ( d1' <> d2' & A' = Line d1',d2' ) by A40, AFF_1:def 3;
A49: ( d1' in A' & d2' in A' ) by A48, AFF_1:26;
d1',d2' // d1',d2' by AFF_1:11;
then d1',d2' // A' by A48, AFF_1:def 4;
then A50: b3',e1' // d1',d2' by A40, A47, AFF_1:45;
reconsider d1 = d1', d2 = d2' as Element of X by ANALMETR:47;
a3',b2' // d1',d2' by A46, A50, AFF_1:14;
then A51: a3,b2 // d1,d2 by ANALMETR:48;
d1,d2 _|_ o,b2 by A4, A41, A49, ANALMETR:78;
then a3,b2 _|_ o,b2 by A48, A51, ANALMETR:84;
then a3,b2 // a3,b3 by A4, A38, ANALMETR:85;
then LIN a3,b2,b3 by ANALMETR:def 11;
then LIN a3',b2',b3' by ANALMETR:55;
then LIN b2',b3',a3' by AFF_1:15;
hence contradiction by A4, A5, A22, AFF_1:39; :: thesis:

end;

then consider c3' being Element of (Af X) such that
A52: ( c3' in A' & LIN b3',e1',c3' ) by A40, AFF_1:73;
reconsider c3 = c3' as Element of X by ANALMETR:47;
A53: b3',e1' // b3',c3' by A52, AFF_1:def 1;
then A54: a3',b2' // b3',c3' by A46, AFF_1:14;
consider e1' being Element of (Af X) such that
A55: ( c3',a3' // a2',e1' & a2' <> e1' ) by DIRAF:47;
not a2',e1' // A'

proof

assume A56: a2',e1' // A' ; :: thesis:
A' // A' by A40, AFF_1:55;
then o',c3' // A' by A40, A52, AFF_1:54;
then a2',e1' // o',c3' by A40, A56, AFF_1:45;
then c3',a3' // o',c3' by A55, AFF_1:14;
then c3',o' // c3',a3' by AFF_1:13;
then A57: LIN c3',o',a3' by AFF_1:def 1;
c3' <> o'

proof

assume c3' = o' ; :: thesis:
then A58: a3',b2' // b3',o' by A46, A53, AFF_1:14;
b3',o' // b3',b2' by A4, A6, AFF_1:53;
then a3',b2' // b3',b2' by A4, A58, AFF_1:14;
then b2',b3' // b2',a3' by AFF_1:13;
then LIN b2',b3',a3' by AFF_1:def 1;
hence contradiction by A4, A5, A22, AFF_1:39; :: thesis:

end;

then A59: a3' in A' by A40, A52, A57, AFF_1:39;
o',a3' // o',a3' by AFF_1:11;
then A' // M' by A4, A5, A40, A59, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A7, A41, ANALMETR:73; :: thesis:

end;

then consider c2' being Element of (Af X) such that
A60: ( c2' in A' & LIN a2',e1',c2' ) by A40, AFF_1:73;
reconsider c2 = c2' as Element of X by ANALMETR:47;
a2',e1' // a2',c2' by A60, AFF_1:def 1;
then c3',a3' // a2',c2' by A55, AFF_1:14;
then A61: ( c2 in A & c3,a3 // a2,c2 ) by A60, ANALMETR:48;
then A62: ( c2 in A & a3,c3 // a2,c2 ) by ANALMETR:81;
consider e1' being Element of (Af X) such that
A63: ( c3',a3' // a1',e1' & a1' <> e1' ) by DIRAF:47;
not a1',e1' // A'

proof

assume A64: a1',e1' // A' ; :: thesis:
A' // A' by A40, AFF_1:55;
then o',c3' // A' by A40, A52, AFF_1:54;
then a1',e1' // o',c3' by A40, A64, AFF_1:45;
then c3',a3' // o',c3' by A63, AFF_1:14;
then c3',o' // c3',a3' by AFF_1:13;
then A65: LIN c3',o',a3' by AFF_1:def 1;
c3' <> o'

proof

assume c3' = o' ; :: thesis:
then A66: a3',b2' // b3',o' by A46, A53, AFF_1:14;
b3',o' // b3',b2' by A4, A6, AFF_1:53;
then a3',b2' // b3',b2' by A4, A66, AFF_1:14;
then b2',b3' // b2',a3' by AFF_1:13;
then LIN b2',b3',a3' by AFF_1:def 1;
hence contradiction by A4, A5, A22, AFF_1:39; :: thesis:

end;

then A67: a3' in A' by A40, A52, A65, AFF_1:39;
o',a3' // o',a3' by AFF_1:11;
then A' // M' by A4, A5, A40, A67, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A7, A41, ANALMETR:73; :: thesis:

end;

then consider c1' being Element of (Af X) such that
A68: ( c1' in A' & LIN a1',e1',c1' ) by A40, AFF_1:73;
reconsider c1 = c1' as Element of X by ANALMETR:47;
a1',e1' // a1',c1' by A68, AFF_1:def 1;
then c3',a3' // a1',c1' by A63, AFF_1:14;
then A69: ( c1 in A & c3,a3 // a1,c1 ) by A68, ANALMETR:48;
then A70: ( c1 in A & a3,c3 // a1,c1 ) by ANALMETR:81;
A71: ( o <> c3 & o <> c2 & o <> c1 )

proof

assume A72: ( o = c3 or o = c2 or o = c1 ) ; :: thesis:

A73: now

assume o = c3 ; :: thesis:
then A74: a3,b2 // b3,o by A54, ANALMETR:48;
b3',o' // b2',b3' by A4, A6, AFF_1:53;
then b3,o // b2,b3 by ANALMETR:48;
then a3,b2 // b2,b3 by A4, A74, ANALMETR:82;
then b2,b3 // b2,a3 by ANALMETR:81;
then LIN b2,b3,a3 by ANALMETR:def 11;
then LIN b2',b3',a3' by ANALMETR:55;
hence contradiction by A4, A5, A22, AFF_1:39; :: thesis:

end;

now

assume ( o = c2 or o = c1 ) ; :: thesis:
then A75: ( a3,c3 // a2,o or a3,c3 // a1,o ) by A61, A69, ANALMETR:81;
( a2',o' // a2',a3' & a1',o' // a2',a3' ) by A4, A6, AFF_1:53;
then ( a2,o // a2,a3 & a1,o // a2,a3 ) by ANALMETR:48;
then a3,c3 // a2,a3 by A4, A75, ANALMETR:82;
then a3,a2 // a3,c3 by ANALMETR:81;
then LIN a3,a2,c3 by ANALMETR:def 11;
then LIN a3',a2',c3' by ANALMETR:55;
then A76: c3' in M' by A4, A5, A21, AFF_1:39;
o',c3' // o',c3' by AFF_1:11;
then A' // M' by A4, A5, A40, A52, A73, A76, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A7, A41, ANALMETR:73; :: thesis:

end;

hence contradiction by A72, A73; :: thesis:

end;

A77: ( not LIN b3,b1,a3 & not LIN b2,b1,a3 )

proof

assume ( LIN b3,b1,a3 or LIN b2,b1,a3 ) ; :: thesis:
then ( LIN b3',b1',a3' or LIN b2',b1',a3' ) by ANALMETR:55;
hence contradiction by A4, A5, A22, AFF_1:39; :: thesis:

end;

A78: ( not LIN a3,a1,c3 & not LIN a3,a2,c3 )

proof

assume ( LIN a3,a1,c3 or LIN a3,a2,c3 ) ; :: thesis:
then ( LIN a3',a1',c3' or LIN a3',a2',c3' ) by ANALMETR:55;
then A79: ( c3' in M' or c3' in M' ) by A4, A5, A21, AFF_1:39;
o',c3' // o',c3' by AFF_1:11;
then A' // M' by A4, A5, A40, A52, A71, A79, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A7, A41, ANALMETR:73; :: thesis:

end;

A80: ( LIN o,a3,a1 & LIN o,b3,b1 & LIN o,a3,a2 & LIN o,b2,b1 & LIN o,a1,a2 & LIN o,b2,b3 )

proof

( o',a3' // o',a1' & o',b3' // o',b1' & o',a3' // o',a2' & o',b2' // o',b1' & o',a1' // o',a2' & o',b2' // o',b3' ) by A4, A6, AFF_1:53;
then ( LIN o',a3',a1' & LIN o',b3',b1' & LIN o',a3',a2' & LIN o',b2',b1' & LIN o',a1',a2' & LIN o',b2',b3' ) by AFF_1:def 1;
hence ( LIN o,a3,a1 & LIN o,b3,b1 & LIN o,a3,a2 & LIN o,b2,b1 & LIN o,a1,a2 & LIN o,b2,b3 ) by ANALMETR:55; :: thesis:

end;

A81: ( LIN o,c3,c1 & LIN o,c3,c2 & LIN o,c1,c2 )

proof

A' // A' by A40, AFF_1:55;
then ( o',c3' // o',c1' & o',c3' // o',c2' & o',c1' // o',c2' ) by A40, A52, A60, A68, AFF_1:53;
then ( LIN o',c3',c1' & LIN o',c3',c2' & LIN o',c1',c2' ) by AFF_1:def 1;
hence ( LIN o,c3,c1 & LIN o,c3,c2 & LIN o,c1,c2 ) by ANALMETR:55; :: thesis:

end;

then b3,c3 // b1,c1 by A2, A4, A70, A71, A77, A78, A80, CONAFFM:def 1;
then A82: c3,b3 // c1,b1 by ANALMETR:81;
b2,c3 // b1,c2 by A2, A4, A62, A71, A77, A78, A80, A81, CONAFFM:def 1;
then A83: c3,b2 // c2,b1 by ANALMETR:81;
A84: not b2 in A

proof

assume A85: b2 in A ; :: thesis:
o',b2' // o',b2' by AFF_1:11;
then A' // N' by A4, A5, A40, A85, AFF_1:52;
then A // N by ANALMETR:64;
hence contradiction by A41, ANALMETR:73; :: thesis:

end;

not c3 in N

proof

assume A86: c3 in N ; :: thesis:
o',c3' // o',c3' by AFF_1:11;
then A' // N' by A4, A5, A40, A52, A71, A86, AFF_1:52;
then A // N by ANALMETR:64;
hence contradiction by A41, ANALMETR:73; :: thesis:

end;

then A87: c1,b2 // c2,b3 by A1, A4, A40, A41, A52, A60, A68, A71, A82, A83, A84, Def1;
A88: not LIN a1,a2,c1

proof

assume LIN a1,a2,c1 ; :: thesis:
then LIN a1',a2',c1' by ANALMETR:55;
then A89: c1' in M' by A4, A5, A21, AFF_1:39;
o',c1' // o',c1' by AFF_1:11;
then A' // M' by A4, A5, A40, A68, A71, A89, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A7, A41, ANALMETR:73; :: thesis:

end;

A90: not LIN c1,c2,b2

proof

assume LIN c1,c2,b2 ; :: thesis:
then A91: LIN c1',c2',b2' by ANALMETR:55;
c1' <> c2'

proof

assume A92: c1' = c2' ; :: thesis:
a3 <> c3

proof

assume A93: a3 = c3 ; :: thesis:
o',c3' // o',c3' by AFF_1:11;
then A' // M' by A4, A5, A40, A52, A93, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A7, A41, ANALMETR:73; :: thesis:

end;

then a2,c1 // a1,c1 by A62, A70, A92, ANALMETR:82;
then c1,a1 // c1,a2 by ANALMETR:81;
then LIN c1,a1,a2 by ANALMETR:def 11;
then LIN c1',a1',a2' by ANALMETR:55;
then LIN a1',a2',c1' by AFF_1:15;
then A94: c1' in M' by A4, A5, A21, AFF_1:39;
o',c1' // o',c1' by AFF_1:11;
then A' // M' by A4, A5, A40, A68, A71, A94, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A7, A41, ANALMETR:73; :: thesis:

end;

hence contradiction by A40, A60, A68, A84, A91, AFF_1:39; :: thesis:

end;

c1,a1 // c2,a2

proof

a3 <> c3

proof

assume A95: a3 = c3 ; :: thesis:
o',a3' // o',a3' by AFF_1:11;
then A' // M' by A4, A5, A40, A52, A95, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A7, A41, ANALMETR:73; :: thesis:

end;

then a2,c2 // a1,c1 by A62, A70, ANALMETR:82;
hence c1,a1 // c2,a2 by ANALMETR:81; :: thesis:

end;

hence a1,b2 // a2,b3 by A2, A4, A71, A80, A81, A87, A88, A90, CONAFFM:def 1; :: thesis:

end;

now

assume A96: not a3,b3 _|_ o,b2 ; :: thesis:
consider x being Element of X such that
A97: ( o,b2 _|_ o,x & o <> x ) by ANALMETR:51;
reconsider x' = x as Element of (Af X) by ANALMETR:47;
LIN o',x',x' by AFF_1:16;
then consider A' being Subset of (Af X) such that
A98: ( A' is being_line & o' in A' & x' in A' & x' in A' ) by AFF_1:33;
reconsider A = A' as Subset of X by ANALMETR:57;
A99: A' // A' by A98, AFF_1:55;
A100: A _|_ N

proof

A101: A = Line o,x

proof

A102: for e1 being Element of X st e1 in A holds
LIN o,x,e1

proof

let e1 be Element of X; :: thesis:
assume A103: e1 in A ; :: thesis:
reconsider e1' = e1 as Element of (Af X) by ANALMETR:47;
A' // A' by A98, AFF_1:55;
then o',x' // o',e1' by A98, A103, AFF_1:53;
then LIN o',x',e1' by AFF_1:def 1;
hence LIN o,x,e1 by ANALMETR:55; :: thesis:

end;

for e1 being Element of X st LIN o,x,e1 holds
e1 in A

proof

let e1 be Element of X; :: thesis:
assume A104: LIN o,x,e1 ; :: thesis:
reconsider e1' = e1 as Element of (Af X) by ANALMETR:47;
LIN o',x',e1' by A104, ANALMETR:55;
hence e1 in A by A97, A98, AFF_1:39; :: thesis:

end;

hence A = Line o,x by A102, ANALMETR:def 12; :: thesis:

end;

o,x _|_ N by A3, A4, A97, ANALMETR:77;
hence A _|_ N by A97, A101, ANALMETR:def 15; :: thesis:

end;

consider e1' being Element of (Af X) such that
A105: ( a3',b3' // b2',e1' & b2' <> e1' ) by DIRAF:47;
not b2',e1' // A'

proof

assume A106: b2',e1' // A' ; :: thesis:
consider d1', d2' being Element of (Af X) such that
A107: ( d1' <> d2' & A' = Line d1',d2' ) by A98, AFF_1:def 3;
A108: ( d1' in A' & d2' in A' ) by A107, AFF_1:26;
d1',d2' // d1',d2' by AFF_1:11;
then d1',d2' // A' by A107, AFF_1:def 4;
then A109: b2',e1' // d1',d2' by A98, A106, AFF_1:45;
reconsider d1 = d1', d2 = d2' as Element of X by ANALMETR:47;
a3',b3' // d1',d2' by A105, A109, AFF_1:14;
then A110: a3,b3 // d1,d2 by ANALMETR:48;
d1,d2 _|_ o,b2 by A4, A100, A108, ANALMETR:78;
hence contradiction by A96, A107, A110, ANALMETR:84; :: thesis:

end;

then consider c3' being Element of (Af X) such that
A111: ( c3' in A' & LIN b2',e1',c3' ) by A98, AFF_1:73;
reconsider c3 = c3' as Element of X by ANALMETR:47;
b2',e1' // b2',c3' by A111, AFF_1:def 1;
then A112: a3',b3' // b2',c3' by A105, AFF_1:14;
consider e1' being Element of (Af X) such that
A113: ( c3',a3' // a1',e1' & a1' <> e1' ) by DIRAF:47;
not a1',e1' // A'

proof

assume A114: a1',e1' // A' ; :: thesis:
A' // A' by A98, AFF_1:55;
then o',c3' // A' by A98, A111, AFF_1:54;
then a1',e1' // o',c3' by A98, A114, AFF_1:45;
then c3',a3' // o',c3' by A113, AFF_1:14;
then c3',o' // c3',a3' by AFF_1:13;
then A115: LIN c3',o',a3' by AFF_1:def 1;
c3' <> o'

proof

assume c3' = o' ; :: thesis:
then A116: a3,b3 // b2,o by A112, ANALMETR:48;
b2',o' // b2',b3' by A4, A6, AFF_1:53;
then b2,o // b2,b3 by ANALMETR:48;
then a3,b3 // b2,b3 by A4, A116, ANALMETR:82;
then b3,b2 // b3,a3 by ANALMETR:81;
then LIN b3,b2,a3 by ANALMETR:def 11;
then LIN b3',b2',a3' by ANALMETR:55;
hence contradiction by A4, A5, A22, AFF_1:39; :: thesis:

end;

then A117: a3' in A' by A98, A111, A115, AFF_1:39;
o',a3' // o',a3' by AFF_1:11;
then A' // M' by A4, A5, A98, A117, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A7, A100, ANALMETR:73; :: thesis:

end;

then consider c1' being Element of (Af X) such that
A118: ( c1' in A' & LIN a1',e1',c1' ) by A98, AFF_1:73;
reconsider c1 = c1' as Element of X by ANALMETR:47;
a1',e1' // a1',c1' by A118, AFF_1:def 1;
then A119: c3',a3' // a1',c1' by A113, AFF_1:14;
then A120: ( c1 in A & c3,a3 // a1,c1 ) by A118, ANALMETR:48;
consider e1' being Element of (Af X) such that
A121: ( c3',a3' // a2',e1' & a2' <> e1' ) by DIRAF:47;
not a2',e1' // A'

proof

assume A122: a2',e1' // A' ; :: thesis:
A' // A' by A98, AFF_1:55;
then o',c3' // A' by A98, A111, AFF_1:54;
then a2',e1' // o',c3' by A98, A122, AFF_1:45;
then c3',a3' // o',c3' by A121, AFF_1:14;
then c3',o' // c3',a3' by AFF_1:13;
then A123: LIN c3',o',a3' by AFF_1:def 1;
c3' <> o'

proof

assume c3' = o' ; :: thesis:
then A124: a3,b3 // b2,o by A112, ANALMETR:48;
b2',o' // b2',b3' by A4, A6, AFF_1:53;
then b2,o // b2,b3 by ANALMETR:48;
then a3,b3 // b2,b3 by A4, A124, ANALMETR:82;
then b3,b2 // b3,a3 by ANALMETR:81;
then LIN b3,b2,a3 by ANALMETR:def 11;
then LIN b3',b2',a3' by ANALMETR:55;
hence contradiction by A4, A5, A22, AFF_1:39; :: thesis:

end;

then A125: a3' in A' by A98, A111, A123, AFF_1:39;
o',a3' // o',a3' by AFF_1:11;
then A' // M' by A4, A5, A98, A125, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A7, A100, ANALMETR:73; :: thesis:

end;

then consider c2' being Element of (Af X) such that
A126: ( c2' in A' & LIN a2',e1',c2' ) by A98, AFF_1:73;
reconsider c2 = c2' as Element of X by ANALMETR:47;
a2',e1' // a2',c2' by A126, AFF_1:def 1;
then A127: c3',a3' // a2',c2' by A121, AFF_1:14;
then A128: ( c2 in A & c3,a3 // a2,c2 ) by A126, ANALMETR:48;
A129: ( o <> c3 & o <> c2 & o <> c1 )

proof

assume A130: ( o = c3 or o = c2 or o = c1 ) ; :: thesis:

A131: now

assume A132: o = c3 ; :: thesis:
b2',o' // b3',b2' by A4, A6, AFF_1:53;
then a3',b3' // b3',b2' by A4, A112, A132, AFF_1:14;
then b3',b2' // b3',a3' by AFF_1:13;
then LIN b3',b2',a3' by AFF_1:def 1;
hence contradiction by A4, A5, A22, AFF_1:39; :: thesis:

end;

now

assume ( o = c2 or o = c1 ) ; :: thesis:
then A133: ( c3,a3 // a1,o or c3,a3 // a2,o ) by A119, A127, ANALMETR:48;
( a1,o // a1,a3 & a2,o // a1,a3 )

proof

( a1',o' // a1',a3' & a2',o' // a1',a3' ) by A4, A6, AFF_1:53;
hence ( a1,o // a1,a3 & a2,o // a1,a3 ) by ANALMETR:48; :: thesis:

end;

then c3,a3 // a1,a3 by A4, A133, ANALMETR:82;
then a3,a1 // a3,c3 by ANALMETR:81;
then LIN a3,a1,c3 by ANALMETR:def 11;
then LIN a3',a1',c3' by ANALMETR:55;
then A134: c3' in M' by A4, A5, A21, AFF_1:39;
o',c3' // o',c3' by AFF_1:11;
then A' // M' by A4, A5, A98, A111, A131, A134, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A7, A100, ANALMETR:73; :: thesis:

end;

hence contradiction by A130, A131; :: thesis:

end;

A135: not LIN a3,a1,c3

proof

assume LIN a3,a1,c3 ; :: thesis:
then LIN a3',a1',c3' by ANALMETR:55;
then A136: c3' in M' by A4, A5, A21, AFF_1:39;
o',c3' // o',c3' by AFF_1:11;
then A' // M' by A4, A5, A98, A111, A129, A136, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A7, A100, ANALMETR:73; :: thesis:

end;

A137: not LIN b3,b1,a3

proof

assume LIN b3,b1,a3 ; :: thesis:
then LIN b3',b1',a3' by ANALMETR:55;
hence contradiction by A4, A5, A22, AFF_1:39; :: thesis:

end;

A138: ( LIN o,a3,a1 & LIN o,b3,b1 & LIN o,a3,a2 & LIN o,b2,b1 & LIN o,a1,a2 & LIN o,b2,b3 )

proof

end;

A139: ( LIN o,c3,c1 & LIN o,c3,c2 & LIN o,c1,c2 )

proof

( o',c3' // o',c1' & o',c3' // o',c2' & o',c1' // o',c2' ) by A98, A99, A111, A118, A126, AFF_1:53;
then ( LIN o',c3',c1' & LIN o',c3',c2' & LIN o',c1',c2' ) by AFF_1:def 1;
hence ( LIN o,c3,c1 & LIN o,c3,c2 & LIN o,c1,c2 ) by ANALMETR:55; :: thesis:

end;

a3,c3 // a1,c1 by A120, ANALMETR:81;
then b3,c3 // b1,c1 by A2, A4, A129, A135, A137, A138, A139, CONAFFM:def 1;
then A140: c3,b3 // c1,b1 by ANALMETR:81;
A141: not LIN b2,b1,a3

proof

assume LIN b2,b1,a3 ; :: thesis:
then LIN b2',b1',a3' by ANALMETR:55;
hence contradiction by A4, A5, A22, AFF_1:39; :: thesis:

end;

A142: not LIN a3,a2,c3

proof

assume LIN a3,a2,c3 ; :: thesis:
then LIN a3',a2',c3' by ANALMETR:55;
then A143: c3' in M' by A4, A5, A21, AFF_1:39;
o',c3' // o',c3' by AFF_1:11;
then A' // M' by A4, A5, A98, A111, A129, A143, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A7, A100, ANALMETR:73; :: thesis:

end;

a3,c3 // a2,c2 by A128, ANALMETR:81;
then b2,c3 // b1,c2 by A2, A4, A129, A138, A139, A141, A142, CONAFFM:def 1;
then A144: c3,b2 // c2,b1 by ANALMETR:81;
A145: not b2 in A

proof

assume A146: b2 in A ; :: thesis:
o',b2' // o',b2' by AFF_1:11;
then A' // N' by A4, A5, A98, A146, AFF_1:52;
then A // N by ANALMETR:64;
hence contradiction by A100, ANALMETR:73; :: thesis:

end;

not c3 in N

proof

assume A147: c3 in N ; :: thesis:
o',c3' // o',c3' by AFF_1:11;
then A' // N' by A4, A5, A98, A111, A129, A147, AFF_1:52;
then A // N by ANALMETR:64;
hence contradiction by A100, ANALMETR:73; :: thesis:

end;

then A148: c1,b2 // c2,b3 by A1, A4, A98, A100, A111, A118, A126, A129, A140, A144, A145, Def1;
A149: not LIN a1,a2,c1

proof

assume LIN a1,a2,c1 ; :: thesis:
then LIN a1',a2',c1' by ANALMETR:55;
then A150: c1' in M' by A4, A5, A21, AFF_1:39;
o',c1' // o',c1' by AFF_1:11;
then M' // A' by A4, A5, A98, A118, A129, A150, AFF_1:52;
then M // A by ANALMETR:64;
hence contradiction by A7, A100, ANALMETR:73; :: thesis:

end;

A151: not LIN c1,c2,b2

proof

assume LIN c1,c2,b2 ; :: thesis:
then A152: LIN c1',c2',b2' by ANALMETR:55;
c1' <> c2'

proof

assume A153: c1' = c2' ; :: thesis:
c3 <> a3

proof

assume A154: c3 = a3 ; :: thesis:
o',c3' // o',c3' by AFF_1:11;
then A' // M' by A4, A5, A98, A111, A154, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A7, A100, ANALMETR:73; :: thesis:

end;

then a1,c1 // a2,c1 by A120, A128, A153, ANALMETR:82;
then c1,a2 // c1,a1 by ANALMETR:81;
then LIN c1,a2,a1 by ANALMETR:def 11;
then LIN c1',a2',a1' by ANALMETR:55;
then LIN a1',a2',c1' by AFF_1:15;
then A155: c1' in M' by A4, A5, A21, AFF_1:39;
o',c1' // o',c1' by AFF_1:11;
then A' // M' by A4, A5, A98, A118, A129, A155, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A7, A100, ANALMETR:73; :: thesis:

end;

then b2' in A' by A98, A118, A126, A152, AFF_1:39;
then A' = N' by A4, A5, A98, AFF_1:30;
then A' // N' by A5, AFF_1:55;
then A // N by ANALMETR:64;
hence contradiction by A100, ANALMETR:73; :: thesis:

end;

c1,a1 // c2,a2

proof

c3 <> a3

proof

assume A156: c3 = a3 ; :: thesis:
o',a3' // o',a3' by AFF_1:11;
then A' // M' by A4, A5, A98, A111, A156, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A7, A100, ANALMETR:73; :: thesis:

end;

then a1,c1 // a2,c2 by A120, A128, ANALMETR:82;
hence c1,a1 // c2,a2 by ANALMETR:81; :: thesis:

end;

hence a1,b2 // a2,b3 by A2, A4, A129, A138, A139, A148, A149, A151, CONAFFM:def 1; :: thesis:

end;

hence a1,b2 // a2,b3 by A37; :: thesis:

end;

hence a1,b2 // a2,b3 by A8, A13, A17; :: thesis:

end;

hence a1,b2 // a2,b3 by A1, A4, Def1; :: thesis: