let X be OrtAfPl; :: thesis:
assume that
A1: X is satisfying_OPAP and
A2: X is satisfying_DES ; :: thesis:
let o be Element of ; :: according to CONMETR:def 2 :: thesis:
let a1, a2, a3, b1, b2, b3 be Element of ; :: thesis:
let M, N be Subset of ; :: thesis:
assume that
A3: M is being_line and
A4: N is being_line and
A5: o in M and
A6: a1 in M and
A7: a2 in M and
A8: a3 in M and
A9: o in N and
A10: b1 in N and
A11: b2 in N and
A12: b3 in N and
A13: not b2 in M and
A14: not a3 in N and
A15: o <> a1 and
A16: o <> a2 and
o <> a3 and
A17: o <> b1 and
o <> b2 and
A18: o <> b3 and
A19: a3,b2 // a2,b1 and
A20: a3,b3 // a1,b1 ; :: thesis:
reconsider o' = o, a1' = a1, a2' = a2, a3' = a3, b1' = b1, b2' = b2, b3' = b3 as Element of by ANALMETR:47;
reconsider M' = M, N' = N as Subset of by ANALMETR:57;
A21: M' is being_line by A3, ANALMETR:58;
A22: N' is being_line by A4, ANALMETR:58;

now

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

A24: now

assume that
A25: a1 <> a2 and
A26: a2 <> a3 and
A27: a1 <> a3 ; :: thesis:
A28: ( b1 <> b2 & b2 <> b3 & b1 <> b3 )

proof

A29: now

A30: not LIN o',b1',a1'

proof

o',a1' // o',a3' by A5, A6, A8, A21, AFF_1:53, AFF_1:55;
then A31: LIN o',a1',a3' by AFF_1:def 1;
assume LIN o',b1',a1' ; :: thesis:
then a1' in N' by A9, A10, A17, A22, AFF_1:39;
hence contradiction by A9, A14, A15, A22, A31, AFF_1:39; :: thesis:

end;

assume b1 = b3 ; :: thesis:
then b1,a1 // b1,a3 by A20, ANALMETR:81;
then A32: b1',a1' // b1',a3' by ANALMETR:48;
o',a1' // o',a3' by A5, A6, A8, A21, AFF_1:53, AFF_1:55;
then LIN o',a1',a3' by AFF_1:def 1;
hence contradiction by A27, A30, A32, AFF_1:23; :: thesis:

end;

A33: now

A34: not LIN o',b1',a1'

proof

o',a1' // o',a3' by A5, A6, A8, A21, AFF_1:53, AFF_1:55;
then A35: LIN o',a1',a3' by AFF_1:def 1;
assume LIN o',b1',a1' ; :: thesis:
then a1' in N' by A9, A10, A17, A22, AFF_1:39;
hence contradiction by A9, A14, A15, A22, A35, AFF_1:39; :: thesis:

end;

assume b2 = b3 ; :: thesis:
then a1,b1 // a2,b1 by A8, A13, A19, A20, ANALMETR:82;
then b1,a1 // b1,a2 by ANALMETR:81;
then A36: b1',a1' // b1',a2' by ANALMETR:48;
o',a1' // o',a2' by A5, A6, A7, A21, AFF_1:53, AFF_1:55;
then LIN o',a1',a2' by AFF_1:def 1;
hence contradiction by A25, A34, A36, AFF_1:23; :: thesis:

end;

A37: now

A38: not LIN o',b2',a2'

proof

assume LIN o',b2',a2' ; :: thesis:
then LIN o',a2',b2' by AFF_1:15;
hence contradiction by A5, A7, A13, A16, A21, AFF_1:39; :: thesis:

end;

assume b1 = b2 ; :: thesis:
then b2,a2 // b2,a3 by A19, ANALMETR:81;
then A39: b2',a2' // b2',a3' by ANALMETR:48;
o',a2' // o',a3' by A5, A7, A8, A21, AFF_1:53, AFF_1:55;
then LIN o',a2',a3' by AFF_1:def 1;
hence contradiction by A26, A38, A39, AFF_1:23; :: thesis:

end;

assume ( b1 = b2 or b2 = b3 or b1 = b3 ) ; :: thesis:
hence contradiction by A37, A33, A29; :: thesis:

end;

A40: now

A41: not LIN b3,b1,a3

proof

assume LIN b3,b1,a3 ; :: thesis:
then LIN b3',b1',a3' by ANALMETR:55;
hence contradiction by A10, A12, A14, A22, A28, AFF_1:39; :: thesis:

end;

o',b2' // o',b3' by A9, A11, A12, A22, AFF_1:53, AFF_1:55;
then LIN o',b2',b3' by AFF_1:def 1;
then A42: LIN o,b2,b3 by ANALMETR:55;
A43: not LIN b2,b1,a3

proof

assume LIN b2,b1,a3 ; :: thesis:
then LIN b2',b1',a3' by ANALMETR:55;
hence contradiction by A10, A11, A14, A22, A28, AFF_1:39; :: thesis:

end;

o',a3' // o',a1' by A5, A6, A8, A21, AFF_1:53, AFF_1:55;
then LIN o',a3',a1' by AFF_1:def 1;
then A44: LIN o,a3,a1 by ANALMETR:55;
consider x being Element of such that
A45: o,b2 _|_ o,x and
A46: o <> x by ANALMETR:51;
A47: o,x _|_ N by A4, A5, A9, A11, A13, A45, ANALMETR:77;
consider e1' being Element of such that
A48: a3',b3' // b2',e1' and
A49: b2' <> e1' by DIRAF:47;
reconsider x' = x as Element of by ANALMETR:47;
LIN o',x',x' by AFF_1:16;
then consider A' being Subset of such that
A50: A' is being_line and
A51: o' in A' and
A52: x' in A' and
x' in A' by AFF_1:33;
reconsider A = A' as Subset of by ANALMETR:57;
A53: for e1 being Element of st e1 in A holds
LIN o,x,e1

proof

let e1 be Element of ; :: thesis:
assume A54: e1 in A ; :: thesis:
reconsider e1' = e1 as Element of by ANALMETR:47;
o',x' // o',e1' by A50, A51, A52, A54, AFF_1:53, AFF_1:55;
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 st LIN o,x,e1 holds
e1 in A

proof

let e1 be Element of ; :: thesis:
assume A55: LIN o,x,e1 ; :: thesis:
reconsider e1' = e1 as Element of by ANALMETR:47;
LIN o',x',e1' by A55, ANALMETR:55;
hence e1 in A by A46, A50, A51, A52, AFF_1:39; :: thesis:

end;

then A = Line o,x by A53, ANALMETR:def 12;
then A56: A _|_ N by A46, A47, ANALMETR:def 15;
A57: not b2 in A

proof

A58: o',b2' // o',b2' by AFF_1:11;
assume b2 in A ; :: thesis:
then A' // N' by A5, A9, A11, A13, A22, A50, A51, A58, AFF_1:52;
then A // N by ANALMETR:64;
hence contradiction by A56, ANALMETR:73; :: thesis:

end;

assume A59: not a3,b3 _|_ o,b2 ; :: thesis:
not b2',e1' // A'

proof

assume A60: b2',e1' // A' ; :: thesis:
consider d1', d2' being Element of such that
A61: d1' <> d2' and
A62: A' = Line d1',d2' by A50, AFF_1:def 3;
A63: d2' in A' by A62, AFF_1:26;
reconsider d1 = d1', d2 = d2' as Element of by ANALMETR:47;
d1',d2' // d1',d2' by AFF_1:11;
then d1',d2' // A' by A61, A62, AFF_1:def 4;
then b2',e1' // d1',d2' by A50, A60, AFF_1:45;
then a3',b3' // d1',d2' by A48, A49, AFF_1:14;
then A64: a3,b3 // d1,d2 by ANALMETR:48;
d1' in A' by A62, AFF_1:26;
then d1,d2 _|_ o,b2 by A9, A11, A56, A63, ANALMETR:78;
hence contradiction by A59, A61, A64, ANALMETR:84; :: thesis:

end;

then consider c3' being Element of such that
A65: c3' in A' and
A66: LIN b2',e1',c3' by A50, AFF_1:73;
b2',e1' // b2',c3' by A66, AFF_1:def 1;
then A67: a3',b3' // b2',c3' by A48, A49, AFF_1:14;
consider e1' being Element of such that
A68: c3',a3' // a1',e1' and
A69: a1' <> e1' by DIRAF:47;
not a1',e1' // A'

proof

A70: c3' <> o'

proof

assume c3' = o' ; :: thesis:
then A71: a3,b3 // b2,o by A67, ANALMETR:48;
b2',o' // b2',b3' by A9, A11, A12, A22, AFF_1:53, AFF_1:55;
then b2,o // b2,b3 by ANALMETR:48;
then a3,b3 // b2,b3 by A5, A13, A71, 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 A11, A12, A14, A22, A28, AFF_1:39; :: thesis:

end;

assume A72: a1',e1' // A' ; :: thesis:
A73: o',a3' // o',a3' by AFF_1:11;
o',c3' // A' by A50, A51, A65, AFF_1:54, AFF_1:55;
then a1',e1' // o',c3' by A50, A72, AFF_1:45;
then c3',a3' // o',c3' by A68, A69, AFF_1:14;
then c3',o' // c3',a3' by AFF_1:13;
then LIN c3',o',a3' by AFF_1:def 1;
then a3' in A' by A50, A51, A65, A70, AFF_1:39;
then A' // M' by A5, A8, A9, A14, A21, A50, A51, A73, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A23, A56, ANALMETR:73; :: thesis:

end;

then consider c1' being Element of such that
A74: c1' in A' and
A75: LIN a1',e1',c1' by A50, AFF_1:73;
reconsider c1 = c1' as Element of by ANALMETR:47;
reconsider c3 = c3' as Element of by ANALMETR:47;
a1',e1' // a1',c1' by A75, AFF_1:def 1;
then A76: c3',a3' // a1',c1' by A68, A69, AFF_1:14;
then A77: c3,a3 // a1,c1 by ANALMETR:48;
consider e1' being Element of such that
A78: c3',a3' // a2',e1' and
A79: a2' <> e1' by DIRAF:47;
not a2',e1' // A'

proof

A80: c3' <> o'

proof

assume c3' = o' ; :: thesis:
then A81: a3,b3 // b2,o by A67, ANALMETR:48;
b2',o' // b2',b3' by A9, A11, A12, A22, AFF_1:53, AFF_1:55;
then b2,o // b2,b3 by ANALMETR:48;
then a3,b3 // b2,b3 by A5, A13, A81, 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 A11, A12, A14, A22, A28, AFF_1:39; :: thesis:

end;

assume A82: a2',e1' // A' ; :: thesis:
A83: o',a3' // o',a3' by AFF_1:11;
o',c3' // A' by A50, A51, A65, AFF_1:54, AFF_1:55;
then a2',e1' // o',c3' by A50, A82, AFF_1:45;
then c3',a3' // o',c3' by A78, A79, AFF_1:14;
then c3',o' // c3',a3' by AFF_1:13;
then LIN c3',o',a3' by AFF_1:def 1;
then a3' in A' by A50, A51, A65, A80, AFF_1:39;
then A' // M' by A5, A8, A9, A14, A21, A50, A51, A83, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A23, A56, ANALMETR:73; :: thesis:

end;

then consider c2' being Element of such that
A84: c2' in A' and
A85: LIN a2',e1',c2' by A50, AFF_1:73;
reconsider c2 = c2' as Element of by ANALMETR:47;
a2',e1' // a2',c2' by A85, AFF_1:def 1;
then A86: c3',a3' // a2',c2' by A78, A79, AFF_1:14;
then A87: c3,a3 // a2,c2 by ANALMETR:48;
A88: ( o <> c3 & o <> c2 & o <> c1 )

proof

A89: now

assume A90: o = c3 ; :: thesis:
b2',o' // b3',b2' by A9, A11, A12, A22, AFF_1:53, AFF_1:55;
then a3',b3' // b3',b2' by A5, A13, A67, A90, 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 A11, A12, A14, A22, A28, AFF_1:39; :: thesis:

end;

A91: now

a1',o' // a1',a3' by A5, A6, A8, A21, AFF_1:53, AFF_1:55;
then A92: a1,o // a1,a3 by ANALMETR:48;
assume ( o = c2 or o = c1 ) ; :: thesis:
then A93: ( c3,a3 // a1,o or c3,a3 // a2,o ) by A76, A86, ANALMETR:48;
a2',o' // a1',a3' by A5, A6, A7, A8, A21, AFF_1:53, AFF_1:55;
then a2,o // a1,a3 by ANALMETR:48;
then c3,a3 // a1,a3 by A15, A16, A93, A92, 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 A94: c3' in M' by A6, A8, A21, A27, AFF_1:39;
o',c3' // o',c3' by AFF_1:11;
then A' // M' by A5, A21, A50, A51, A65, A89, A94, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A23, A56, ANALMETR:73; :: thesis:

end;

assume ( o = c3 or o = c2 or o = c1 ) ; :: thesis:
hence contradiction by A89, A91; :: thesis:

end;

A95: not c3 in N

proof

A96: o',c3' // o',c3' by AFF_1:11;
assume c3 in N ; :: thesis:
then A' // N' by A9, A22, A50, A51, A65, A88, A96, AFF_1:52;
then A // N by ANALMETR:64;
hence contradiction by A56, ANALMETR:73; :: thesis:

end;

A97: not LIN a3,a2,c3

proof

assume LIN a3,a2,c3 ; :: thesis:
then LIN a3',a2',c3' by ANALMETR:55;
then A98: c3' in M' by A7, A8, A21, A26, AFF_1:39;
o',c3' // o',c3' by AFF_1:11;
then A' // M' by A5, A21, A50, A51, A65, A88, A98, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A23, A56, ANALMETR:73; :: thesis:

end;

A99: not LIN a3,a1,c3

proof

assume LIN a3,a1,c3 ; :: thesis:
then LIN a3',a1',c3' by ANALMETR:55;
then A100: c3' in M' by A6, A8, A21, A27, AFF_1:39;
o',c3' // o',c3' by AFF_1:11;
then A' // M' by A5, A21, A50, A51, A65, A88, A100, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A23, A56, ANALMETR:73; :: thesis:

end;

A101: not LIN a1,a2,c1

proof

assume LIN a1,a2,c1 ; :: thesis:
then LIN a1',a2',c1' by ANALMETR:55;
then A102: c1' in M' by A6, A7, A21, A25, AFF_1:39;
o',c1' // o',c1' by AFF_1:11;
then M' // A' by A5, A21, A50, A51, A74, A88, A102, AFF_1:52;
then M // A by ANALMETR:64;
hence contradiction by A23, A56, ANALMETR:73; :: thesis:

end;

o',a1' // o',a2' by A5, A6, A7, A21, AFF_1:53, AFF_1:55;
then LIN o',a1',a2' by AFF_1:def 1;
then A103: LIN o,a1,a2 by ANALMETR:55;
o',b2' // o',b1' by A9, A10, A11, A22, AFF_1:53, AFF_1:55;
then LIN o',b2',b1' by AFF_1:def 1;
then A104: LIN o,b2,b1 by ANALMETR:55;
o',c1' // o',c2' by A50, A51, A74, A84, AFF_1:53, AFF_1:55;
then LIN o',c1',c2' by AFF_1:def 1;
then A105: LIN o,c1,c2 by ANALMETR:55;
o',c3' // o',c2' by A50, A51, A65, A84, AFF_1:53, AFF_1:55;
then LIN o',c3',c2' by AFF_1:def 1;
then A106: LIN o,c3,c2 by ANALMETR:55;
o',c3' // o',c1' by A50, A51, A65, A74, AFF_1:53, AFF_1:55;
then LIN o',c3',c1' by AFF_1:def 1;
then A107: LIN o,c3,c1 by ANALMETR:55;
c3 <> a3

proof

A108: o',a3' // o',a3' by AFF_1:11;
assume c3 = a3 ; :: thesis:
then A' // M' by A5, A8, A9, A14, A21, A50, A51, A65, A108, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A23, A56, ANALMETR:73; :: thesis:

end;

then a1,c1 // a2,c2 by A77, A87, ANALMETR:82;
then A109: c1,a1 // c2,a2 by ANALMETR:81;
A110: not LIN c1,c2,b2

proof

A111: c1' <> c2'

proof

A112: c3 <> a3

proof

A113: o',c3' // o',c3' by AFF_1:11;
assume c3 = a3 ; :: thesis:
then A' // M' by A5, A8, A9, A14, A21, A50, A51, A65, A113, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A23, A56, ANALMETR:73; :: thesis:

end;

assume c1' = c2' ; :: thesis:
then a1,c1 // a2,c1 by A77, A87, A112, 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 A114: c1' in M' by A6, A7, A21, A25, AFF_1:39;
o',c1' // o',c1' by AFF_1:11;
then A' // M' by A5, A21, A50, A51, A74, A88, A114, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A23, A56, ANALMETR:73; :: thesis:

end;

assume LIN c1,c2,b2 ; :: thesis:
then LIN c1',c2',b2' by ANALMETR:55;
then b2' in A' by A50, A74, A84, A111, AFF_1:39;
then A' = N' by A5, A9, A11, A13, A22, A50, A51, AFF_1:30;
then A' // N' by A22, AFF_1:55;
then A // N by ANALMETR:64;
hence contradiction by A56, ANALMETR:73; :: thesis:

end;

o',a3' // o',a2' by A5, A7, A8, A21, AFF_1:53, AFF_1:55;
then LIN o',a3',a2' by AFF_1:def 1;
then A115: LIN o,a3,a2 by ANALMETR:55;
o',b3' // o',b1' by A9, A10, A12, A22, AFF_1:53, AFF_1:55;
then LIN o',b3',b1' by AFF_1:def 1;
then A116: LIN o,b3,b1 by ANALMETR:55;
a3,c3 // a1,c1 by A77, ANALMETR:81;
then b3,c3 // b1,c1 by A2, A9, A14, A15, A17, A18, A20, A88, A99, A41, A44, A116, A107, CONAFFM:def 1;
then A117: c3,b3 // c1,b1 by ANALMETR:81;
a3,c3 // a2,c2 by A87, ANALMETR:81;
then b2,c3 // b1,c2 by A2, A5, A9, A13, A14, A16, A17, A19, A88, A115, A104, A106, A43, A97, CONAFFM:def 1;
then c3,b2 // c2,b1 by ANALMETR:81;
then c1,b2 // c2,b3 by A1, A9, A10, A11, A12, A17, A18, A51, A56, A65, A74, A84, A88, A117, A57, A95, Def1;
hence a1,b2 // a2,b3 by A2, A5, A13, A15, A16, A18, A88, A103, A42, A105, A101, A110, A109, CONAFFM:def 1; :: thesis:

end;

now

o',a1' // o',a2' by A5, A6, A7, A21, AFF_1:53, AFF_1:55;
then LIN o',a1',a2' by AFF_1:def 1;
then A118: LIN o,a1,a2 by ANALMETR:55;
o',b2' // o',b1' by A9, A10, A11, A22, AFF_1:53, AFF_1:55;
then LIN o',b2',b1' by AFF_1:def 1;
then A119: LIN o,b2,b1 by ANALMETR:55;
o',b2' // o',b3' by A9, A11, A12, A22, AFF_1:53, AFF_1:55;
then LIN o',b2',b3' by AFF_1:def 1;
then A120: LIN o,b2,b3 by ANALMETR:55;
A121: ( 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 A10, A11, A12, A14, A22, A28, AFF_1:39; :: thesis:

end;

o',a3' // o',a2' by A5, A7, A8, A21, AFF_1:53, AFF_1:55;
then LIN o',a3',a2' by AFF_1:def 1;
then A122: LIN o,a3,a2 by ANALMETR:55;
o',b3' // o',b1' by A9, A10, A12, A22, AFF_1:53, AFF_1:55;
then LIN o',b3',b1' by AFF_1:def 1;
then A123: LIN o,b3,b1 by ANALMETR:55;
o',a3' // o',a1' by A5, A6, A8, A21, AFF_1:53, AFF_1:55;
then LIN o',a3',a1' by AFF_1:def 1;
then A124: LIN o,a3,a1 by ANALMETR:55;
consider x being Element of such that
A125: o,b2 _|_ o,x and
A126: o <> x by ANALMETR:51;
A127: o,x _|_ N by A4, A5, A9, A11, A13, A125, ANALMETR:77;
consider e1' being Element of such that
A128: a3',b2' // b3',e1' and
A129: b3' <> e1' by DIRAF:47;
reconsider x' = x as Element of by ANALMETR:47;
LIN o',x',x' by AFF_1:16;
then consider A' being Subset of such that
A130: A' is being_line and
A131: o' in A' and
A132: x' in A' and
x' in A' by AFF_1:33;
reconsider A = A' as Subset of by ANALMETR:57;
A133: for e1 being Element of st e1 in A holds
LIN o,x,e1

proof

let e1 be Element of ; :: thesis:
assume A134: e1 in A ; :: thesis:
reconsider e1' = e1 as Element of by ANALMETR:47;
o',x' // o',e1' by A130, A131, A132, A134, AFF_1:53, AFF_1:55;
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 st LIN o,x,e1 holds
e1 in A

proof

let e1 be Element of ; :: thesis:
assume A135: LIN o,x,e1 ; :: thesis:
reconsider e1' = e1 as Element of by ANALMETR:47;
LIN o',x',e1' by A135, ANALMETR:55;
hence e1 in A by A126, A130, A131, A132, AFF_1:39; :: thesis:

end;

then A = Line o,x by A133, ANALMETR:def 12;
then A136: A _|_ N by A126, A127, ANALMETR:def 15;
assume A137: a3,b3 _|_ o,b2 ; :: thesis:
not b3',e1' // A'

proof

assume A138: b3',e1' // A' ; :: thesis:
consider d1', d2' being Element of such that
A139: d1' <> d2' and
A140: A' = Line d1',d2' by A130, AFF_1:def 3;
A141: d2' in A' by A140, AFF_1:26;
reconsider d1 = d1', d2 = d2' as Element of by ANALMETR:47;
d1',d2' // d1',d2' by AFF_1:11;
then d1',d2' // A' by A139, A140, AFF_1:def 4;
then b3',e1' // d1',d2' by A130, A138, AFF_1:45;
then a3',b2' // d1',d2' by A128, A129, AFF_1:14;
then A142: a3,b2 // d1,d2 by ANALMETR:48;
d1' in A' by A140, AFF_1:26;
then d1,d2 _|_ o,b2 by A9, A11, A136, A141, ANALMETR:78;
then a3,b2 _|_ o,b2 by A139, A142, ANALMETR:84;
then a3,b2 // a3,b3 by A5, A13, A137, 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 A11, A12, A14, A22, A28, AFF_1:39; :: thesis:

end;

then consider c3' being Element of such that
A143: c3' in A' and
A144: LIN b3',e1',c3' by A130, AFF_1:73;
A145: b3',e1' // b3',c3' by A144, AFF_1:def 1;
consider e1' being Element of such that
A146: c3',a3' // a2',e1' and
A147: a2' <> e1' by DIRAF:47;
not a2',e1' // A'

proof

A148: c3' <> o'

proof

assume c3' = o' ; :: thesis:
then A149: a3',b2' // b3',o' by A128, A129, A145, AFF_1:14;
b3',o' // b3',b2' by A9, A11, A12, A22, AFF_1:53, AFF_1:55;
then a3',b2' // b3',b2' by A18, A149, 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 A11, A12, A14, A22, A28, AFF_1:39; :: thesis:

end;

assume A150: a2',e1' // A' ; :: thesis:
A151: o',a3' // o',a3' by AFF_1:11;
o',c3' // A' by A130, A131, A143, AFF_1:54, AFF_1:55;
then a2',e1' // o',c3' by A130, A150, AFF_1:45;
then c3',a3' // o',c3' by A146, A147, AFF_1:14;
then c3',o' // c3',a3' by AFF_1:13;
then LIN c3',o',a3' by AFF_1:def 1;
then a3' in A' by A130, A131, A143, A148, AFF_1:39;
then A' // M' by A5, A8, A9, A14, A21, A130, A131, A151, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A23, A136, ANALMETR:73; :: thesis:

end;

then consider c2' being Element of such that
A152: c2' in A' and
A153: LIN a2',e1',c2' by A130, AFF_1:73;
reconsider c3 = c3' as Element of by ANALMETR:47;
reconsider c2 = c2' as Element of by ANALMETR:47;
a2',e1' // a2',c2' by A153, AFF_1:def 1;
then c3',a3' // a2',c2' by A146, A147, AFF_1:14;
then A154: c3,a3 // a2,c2 by ANALMETR:48;
then A155: a3,c3 // a2,c2 by ANALMETR:81;
consider e1' being Element of such that
A156: c3',a3' // a1',e1' and
A157: a1' <> e1' by DIRAF:47;
not a1',e1' // A'

proof

A158: c3' <> o'

proof

assume c3' = o' ; :: thesis:
then A159: a3',b2' // b3',o' by A128, A129, A145, AFF_1:14;
b3',o' // b3',b2' by A9, A11, A12, A22, AFF_1:53, AFF_1:55;
then a3',b2' // b3',b2' by A18, A159, 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 A11, A12, A14, A22, A28, AFF_1:39; :: thesis:

end;

assume A160: a1',e1' // A' ; :: thesis:
A161: o',a3' // o',a3' by AFF_1:11;
o',c3' // A' by A130, A131, A143, AFF_1:54, AFF_1:55;
then a1',e1' // o',c3' by A130, A160, AFF_1:45;
then c3',a3' // o',c3' by A156, A157, AFF_1:14;
then c3',o' // c3',a3' by AFF_1:13;
then LIN c3',o',a3' by AFF_1:def 1;
then a3' in A' by A130, A131, A143, A158, AFF_1:39;
then A' // M' by A5, A8, A9, A14, A21, A130, A131, A161, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A23, A136, ANALMETR:73; :: thesis:

end;

then consider c1' being Element of such that
A162: c1' in A' and
A163: LIN a1',e1',c1' by A130, AFF_1:73;
reconsider c1 = c1' as Element of by ANALMETR:47;
a1',e1' // a1',c1' by A163, AFF_1:def 1;
then c3',a3' // a1',c1' by A156, A157, AFF_1:14;
then A164: c3,a3 // a1,c1 by ANALMETR:48;
then A165: a3,c3 // a1,c1 by ANALMETR:81;
A166: a3',b2' // b3',c3' by A128, A129, A145, AFF_1:14;
A167: ( o <> c3 & o <> c2 & o <> c1 )

proof

A168: now

assume o = c3 ; :: thesis:
then A169: a3,b2 // b3,o by A166, ANALMETR:48;
b3',o' // b2',b3' by A9, A11, A12, A22, AFF_1:53, AFF_1:55;
then b3,o // b2,b3 by ANALMETR:48;
then a3,b2 // b2,b3 by A18, A169, 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 A11, A12, A14, A22, A28, AFF_1:39; :: thesis:

end;

A170: now

a2',o' // a2',a3' by A5, A7, A8, A21, AFF_1:53, AFF_1:55;
then A171: a2,o // a2,a3 by ANALMETR:48;
assume ( o = c2 or o = c1 ) ; :: thesis:
then A172: ( a3,c3 // a2,o or a3,c3 // a1,o ) by A154, A164, ANALMETR:81;
a1',o' // a2',a3' by A5, A6, A7, A8, A21, AFF_1:53, AFF_1:55;
then a1,o // a2,a3 by ANALMETR:48;
then a3,c3 // a2,a3 by A15, A16, A172, A171, 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 A173: c3' in M' by A7, A8, A21, A26, AFF_1:39;
o',c3' // o',c3' by AFF_1:11;
then A' // M' by A5, A21, A130, A131, A143, A168, A173, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A23, A136, ANALMETR:73; :: thesis:

end;

assume ( o = c3 or o = c2 or o = c1 ) ; :: thesis:
hence contradiction by A168, A170; :: thesis:

end;

A174: not c3 in N

proof

A175: o',c3' // o',c3' by AFF_1:11;
assume c3 in N ; :: thesis:
then A' // N' by A9, A22, A130, A131, A143, A167, A175, AFF_1:52;
then A // N by ANALMETR:64;
hence contradiction by A136, ANALMETR:73; :: thesis:

end;

A176: not LIN a1,a2,c1

proof

assume LIN a1,a2,c1 ; :: thesis:
then LIN a1',a2',c1' by ANALMETR:55;
then A177: c1' in M' by A6, A7, A21, A25, AFF_1:39;
o',c1' // o',c1' by AFF_1:11;
then A' // M' by A5, A21, A130, A131, A162, A167, A177, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A23, A136, ANALMETR:73; :: thesis:

end;

A178: ( 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 A179: ( c3' in M' or c3' in M' ) by A6, A7, A8, A21, A26, A27, AFF_1:39;
o',c3' // o',c3' by AFF_1:11;
then A' // M' by A5, A21, A130, A131, A143, A167, A179, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A23, A136, ANALMETR:73; :: thesis:

end;

A180: not b2 in A

proof

A181: o',b2' // o',b2' by AFF_1:11;
assume b2 in A ; :: thesis:
then A' // N' by A5, A9, A11, A13, A22, A130, A131, A181, AFF_1:52;
then A // N by ANALMETR:64;
hence contradiction by A136, ANALMETR:73; :: thesis:

end;

A182: not LIN c1,c2,b2

proof

A183: c1' <> c2'

proof

A184: a3 <> c3

proof

A185: o',c3' // o',c3' by AFF_1:11;
assume a3 = c3 ; :: thesis:
then A' // M' by A5, A8, A9, A14, A21, A130, A131, A143, A185, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A23, A136, ANALMETR:73; :: thesis:

end;

assume c1' = c2' ; :: thesis:
then a2,c1 // a1,c1 by A155, A165, A184, 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 A186: c1' in M' by A6, A7, A21, A25, AFF_1:39;
o',c1' // o',c1' by AFF_1:11;
then A' // M' by A5, A21, A130, A131, A162, A167, A186, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A23, A136, ANALMETR:73; :: thesis:

end;

assume LIN c1,c2,b2 ; :: thesis:
then LIN c1',c2',b2' by ANALMETR:55;
hence contradiction by A130, A152, A162, A180, A183, AFF_1:39; :: thesis:

end;

o',c1' // o',c2' by A130, A131, A152, A162, AFF_1:53, AFF_1:55;
then LIN o',c1',c2' by AFF_1:def 1;
then A187: LIN o,c1,c2 by ANALMETR:55;
a3 <> c3

proof

A188: o',a3' // o',a3' by AFF_1:11;
assume a3 = c3 ; :: thesis:
then A' // M' by A5, A8, A9, A14, A21, A130, A131, A143, A188, AFF_1:52;
then A // M by ANALMETR:64;
hence contradiction by A23, A136, ANALMETR:73; :: thesis:

end;

then a2,c2 // a1,c1 by A155, A165, ANALMETR:82;
then A189: c1,a1 // c2,a2 by ANALMETR:81;
o',c3' // o',c1' by A130, A131, A143, A162, AFF_1:53, AFF_1:55;
then LIN o',c3',c1' by AFF_1:def 1;
then LIN o,c3,c1 by ANALMETR:55;
then b3,c3 // b1,c1 by A2, A9, A14, A15, A17, A18, A20, A165, A167, A121, A178, A124, A123, CONAFFM:def 1;
then A190: c3,b3 // c1,b1 by ANALMETR:81;
o',c3' // o',c2' by A130, A131, A143, A152, AFF_1:53, AFF_1:55;
then LIN o',c3',c2' by AFF_1:def 1;
then LIN o,c3,c2 by ANALMETR:55;
then b2,c3 // b1,c2 by A2, A5, A9, A13, A14, A16, A17, A19, A155, A167, A121, A178, A122, A119, CONAFFM:def 1;
then c3,b2 // c2,b1 by ANALMETR:81;
then c1,b2 // c2,b3 by A1, A9, A10, A11, A12, A17, A18, A131, A136, A143, A152, A162, A167, A190, A180, A174, Def1;
hence a1,b2 // a2,b3 by A2, A5, A13, A15, A16, A18, A167, A118, A120, A187, A176, A182, A189, CONAFFM:def 1; :: thesis:

end;

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

end;

A191: now

A192: not LIN o',a3',b3'

proof

assume LIN o',a3',b3' ; :: thesis:
then LIN o',b3',a3' by AFF_1:15;
hence contradiction by A9, A12, A14, A18, A22, AFF_1:39; :: thesis:

end;

o',b3' // o',b1' by A9, A10, A12, A22, AFF_1:53, AFF_1:55;
then A193: LIN o',b3',b1' by AFF_1:def 1;
assume A194: a1 = a3 ; :: thesis:
then a3',b3' // a3',b1' by A20, ANALMETR:48;
hence a1,b2 // a2,b3 by A19, A194, A192, A193, AFF_1:23; :: thesis:

end;

A195: now

o',b2' // o',b3' by A9, A11, A12, A22, AFF_1:53, AFF_1:55;
then A196: LIN o',b2',b3' by AFF_1:def 1;
assume A197: a1 = a2 ; :: thesis:
a1 <> b1

proof

o',a1' // o',a3' by A5, A6, A8, A21, AFF_1:53, AFF_1:55;
then A198: LIN o',a1',a3' by AFF_1:def 1;
assume a1 = b1 ; :: thesis:
hence contradiction by A9, A10, A14, A15, A22, A198, AFF_1:39; :: thesis:

end;

then a3,b2 // a3,b3 by A19, A20, A197, ANALMETR:82;
then a3',b2' // a3',b3' by ANALMETR:48;
then b2' = b3' by A5, A8, A9, A13, A14, A21, A196, AFF_1:23, AFF_1:39;
then a1',b2' // a2',b3' by A197, AFF_1:11;
hence a1,b2 // a2,b3 by ANALMETR:48; :: thesis:

end;

now

o',b2' // o',b1' by A9, A10, A11, A22, AFF_1:53, AFF_1:55;
then A199: LIN o',b2',b1' by AFF_1:def 1;
assume A200: a2 = a3 ; :: thesis:
then a3',b2' // a3',b1' by A19, ANALMETR:48;
then b2' = b1' by A5, A8, A9, A13, A14, A21, A199, AFF_1:23, AFF_1:39;
hence a1,b2 // a2,b3 by A20, A200, ANALMETR:81; :: thesis:

end;

hence a1,b2 // a2,b3 by A195, A191, A24; :: thesis:

end;

hence a1,b2 // a2,b3 by A1, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, Def1; :: thesis: