let X be OrtAfPl; :: thesis: ( X is satisfying_3H implies X is satisfying_OPAP )
assume A1: X is satisfying_3H ; :: thesis: X is satisfying_OPAP
let o be Element of ; :: according to CONMETR:def 1 :: thesis: for a1, a2, a3, b1, b2, b3 being Element of
for M, N being Subset of st 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 & M _|_ N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 holds
a1,b2 // a2,b3
let a1, a2, a3, b1, b2, b3 be Element of ; :: thesis: for M, N being Subset of st 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 & M _|_ N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 holds
a1,b2 // a2,b3
let M, N be Subset of ; :: thesis: ( 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 & M _|_ N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 implies a1,b2 // a2,b3 )
assume that
A2: o in M and
A3: a1 in M and
A4: a2 in M and
A5: a3 in M and
A6: o in N and
A7: b1 in N and
A8: b2 in N and
A9: b3 in N and
A10: not b2 in M and
A11: not a3 in N and
A12: M _|_ N and
A13: o <> a1 and
A14: o <> a2 and
o <> a3 and
A15: o <> b1 and
o <> b2 and
A16: o <> b3 and
A17: a3,b2 // a2,b1 and
A18: a3,b3 // a1,b1 ; :: thesis: a1,b2 // a2,b3
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;
N is being_line by A12, ANALMETR:62;
then A19: N' is being_line by ANALMETR:58;
M is being_line by A12, ANALMETR:62;
then A20: M' is being_line by ANALMETR:58;

A21: now

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

proof

o',a1' // o',a3' by A2, A3, A5, A20, AFF_1:53, AFF_1:55;
then A23: LIN o',a1',a3' by AFF_1:def 1;
assume LIN o',b1',a1' ; :: thesis: contradiction
then a1' in N' by A6, A7, A15, A19, AFF_1:39;
hence contradiction by A6, A11, A13, A19, A23, AFF_1:39; :: thesis: verum

end;

A24: b1,a2 // a3,b2 by A17, ANALMETR:81;
o',a1' // o',a2' by A2, A3, A4, A20, AFF_1:53, AFF_1:55;
then A25: LIN o',a1',a2' by AFF_1:def 1;
assume A26: b2 = b3 ; :: thesis: a1,b2 // a2,b3
then b1,a1 // a3,b2 by A18, ANALMETR:81;
then b1,a1 // b1,a2 by A5, A10, A24, ANALMETR:82;
then b1',a1' // b1',a2' by ANALMETR:48;
then a1' = a2' by A22, A25, AFF_1:23;
then a1',b2' // a2',b3' by A26, AFF_1:11;
hence a1,b2 // a2,b3 by ANALMETR:48; :: thesis: verum

end;

A27: for a, b, c being Element of st LIN a,b,c holds
( LIN a,c,b & LIN b,a,c & LIN b,c,a & LIN c,a,b & LIN c,b,a )

proof

let a, b, c be Element of ; :: thesis: ( LIN a,b,c implies ( LIN a,c,b & LIN b,a,c & LIN b,c,a & LIN c,a,b & LIN c,b,a ) )
reconsider a' = a, b' = b, c' = c as Element of by ANALMETR:47;
assume LIN a,b,c ; :: thesis: ( LIN a,c,b & LIN b,a,c & LIN b,c,a & LIN c,a,b & LIN c,b,a )
then A28: LIN a',b',c' by ANALMETR:55;
then A29: LIN b',a',c' by AFF_1:15;
A30: LIN c',a',b' by A28, AFF_1:15;
A31: LIN b',c',a' by A28, AFF_1:15;
A32: LIN c',b',a' by A28, AFF_1:15;
LIN a',c',b' by A28, AFF_1:15;
hence ( LIN a,c,b & LIN b,a,c & LIN b,c,a & LIN c,a,b & LIN c,b,a ) by A29, A31, A30, A32, ANALMETR:55; :: thesis: verum

end;

A33: now

o',a3' // o',a1' by A2, A3, A5, A20, AFF_1:53, AFF_1:55;
then LIN o',a3',a1' by AFF_1:def 1;
then A34: LIN o,a3,a1 by ANALMETR:55;
a3',a1' // a3',a2' by A3, A4, A5, A20, AFF_1:53, AFF_1:55;
then LIN a3',a1',a2' by AFF_1:def 1;
then A35: LIN a3,a1,a2 by ANALMETR:55;
o',b2' // o',b3' by A6, A8, A9, A19, AFF_1:53, AFF_1:55;
then LIN o',b2',b3' by AFF_1:def 1;
then A36: LIN o,b2,b3 by ANALMETR:55;
assume that
A37: a1 <> a3 and
A38: b2 <> b3 ; :: thesis: a1,b2 // a2,b3
A39: ( not LIN a3,a1,b2 & not LIN b2,a3,b3 )

proof

assume ( LIN a3,a1,b2 or LIN b2,a3,b3 ) ; :: thesis: contradiction
then ( LIN a3',a1',b2' or LIN b2',a3',b3' ) by ANALMETR:55;
then ( LIN a3',a1',b2' or LIN b2',b3',a3' ) by AFF_1:15;
hence contradiction by A3, A5, A8, A9, A10, A11, A20, A19, A37, A38, AFF_1:39; :: thesis: verum

end;

b2',b3' // b2',b1' by A7, A8, A9, A19, AFF_1:53, AFF_1:55;
then LIN b2',b3',b1' by AFF_1:def 1;
then A40: LIN b2,b3,b1 by ANALMETR:55;

A41: now

assume A42: b2 <> b1 ; :: thesis: a1,b2 // a2,b3
not LIN a2,a3,b3

proof

A43: a3 <> a2

proof

assume a3 = a2 ; :: thesis: contradiction
then LIN a3,b2,b1 by A17, ANALMETR:def 11;
then LIN b2,b1,a3 by A27;
then A44: b2,b1 // b2,a3 by ANALMETR:def 11;
LIN b2,b1,b3 by A27, A40;
then b2,b1 // b2,b3 by ANALMETR:def 11;
then b2,a3 // b2,b3 by A42, A44, ANALMETR:82;
hence contradiction by A39, ANALMETR:def 11; :: thesis: verum

end;

LIN a3,a1,o by A27, A34;
then A45: a3,a1 // a3,o by ANALMETR:def 11;
A46: a3 <> a1

proof

assume a3 = a1 ; :: thesis: contradiction
then LIN a3',a1',b2' by AFF_1:16;
hence contradiction by A39, ANALMETR:55; :: thesis: verum

end;

assume LIN a2,a3,b3 ; :: thesis: contradiction
then LIN a3,a2,b3 by A27;
then A47: a3,a2 // a3,b3 by ANALMETR:def 11;
LIN a3,a2,a1 by A27, A35;
then a3,a2 // a3,a1 by ANALMETR:def 11;
then a3,a1 // a3,b3 by A47, A43, ANALMETR:82;
then a3,o // a3,b3 by A46, A45, ANALMETR:82;
then a3',o' // a3',b3' by ANALMETR:48;
then A48: a3',b3' // a3',o' by AFF_1:13;
LIN b2,b3,o by A27, A36;
then A49: LIN b2',b3',o' by ANALMETR:55;
not LIN b2',a3',b3' by A39, ANALMETR:55;
hence contradiction by A16, A48, A49, AFF_1:23; :: thesis: verum

end;

then consider c1 being Element of such that
A50: c1,a2 _|_ a3,b3 and
A51: c1,a3 _|_ a2,b3 and
A52: c1,b3 _|_ a2,a3 by A1, CONAFFM:def 3;
reconsider c1' = c1 as Element of by ANALMETR:47;

A53: now

A54: a2 <> a3

proof

A55: not LIN o',a3',b1'

proof

assume LIN o',a3',b1' ; :: thesis: contradiction
then LIN o',b1',a3' by AFF_1:15;
hence contradiction by A6, A7, A11, A15, A19, AFF_1:39; :: thesis: verum

end;

assume a2 = a3 ; :: thesis: contradiction
then a3',b2' // a3',b1' by A17, ANALMETR:48;
then A56: a3',b1' // a3',b2' by AFF_1:13;
o',b1' // o',b2' by A6, A7, A8, A19, AFF_1:53, AFF_1:55;
then LIN o',b1',b2' by AFF_1:def 1;
hence contradiction by A42, A55, A56, AFF_1:23; :: thesis: verum

end;

a2,a3 _|_ b2,b3 by A4, A5, A8, A9, A12, ANALMETR:78;
then b2,b3 // c1,b3 by A52, A54, ANALMETR:85;
then b3,b2 // b3,c1 by ANALMETR:81;
then LIN b3,b2,c1 by ANALMETR:def 11;
then LIN b3',b2',c1' by ANALMETR:55;
then A57: c1 in N by A8, A9, A19, A38, AFF_1:39;
A58: not LIN o',a2',c1'

proof

A59: o' <> c1'

proof

assume A60: o' = c1' ; :: thesis: contradiction
o,a2 _|_ b3,b2 by A2, A4, A8, A9, A12, ANALMETR:78;
then b3,b2 // a3,b3 by A14, A50, A60, ANALMETR:85;
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 A8, A9, A11, A19, A38, AFF_1:39; :: thesis: verum

end;

o',a2' // o',a3' by A2, A4, A5, A20, AFF_1:53, AFF_1:55;
then A61: LIN o',a2',a3' by AFF_1:def 1;
assume LIN o',a2',c1' ; :: thesis: contradiction
then LIN o',c1',a2' by AFF_1:15;
then a2' in N' by A6, A19, A57, A59, AFF_1:39;
hence contradiction by A6, A11, A14, A19, A61, AFF_1:39; :: thesis: verum

end;

A62: a1 <> b1

proof

o',b1' // o',b2' by A6, A7, A8, A19, AFF_1:53, AFF_1:55;
then A63: LIN o',b1',b2' by AFF_1:def 1;
assume a1 = b1 ; :: thesis: contradiction
hence contradiction by A2, A3, A10, A13, A20, A63, AFF_1:39; :: thesis: verum

end;

assume A64: a2 <> a1 ; :: thesis: a1,b2 // a2,b3
A65: a1 <> b1

proof

LIN a1,a2,a3 by A27, A35;
then a1,a2 // a1,a3 by ANALMETR:def 11;
then A66: a2,a1 // a3,a1 by ANALMETR:81;
assume a1 = b1 ; :: thesis: contradiction
then a3,a1 // a3,b2 by A17, A64, A66, ANALMETR:82;
hence contradiction by A39, ANALMETR:def 11; :: thesis: verum

end;

not LIN a2,a1,b1

proof

assume LIN a2,a1,b1 ; :: thesis: contradiction
then LIN b1,a1,a2 by A27;
then b1,a1 // b1,a2 by ANALMETR:def 11;
then a1,b1 // a2,b1 by ANALMETR:81;
then A67: a2,b1 // a3,b3 by A18, A65, ANALMETR:82;
a2 <> b1

proof

o',b1' // o',b2' by A6, A7, A8, A19, AFF_1:53, AFF_1:55;
then A68: LIN o',b1',b2' by AFF_1:def 1;
assume a2 = b1 ; :: thesis: contradiction
hence contradiction by A2, A4, A10, A14, A20, A68, AFF_1:39; :: thesis: verum

end;

then a3,b3 // a3,b2 by A17, A67, ANALMETR:82;
then LIN a3,b3,b2 by ANALMETR:def 11;
hence contradiction by A27, A39; :: thesis: verum

end;

then consider c2 being Element of such that
A69: c2,a2 _|_ a1,b1 and
A70: c2,a1 _|_ a2,b1 and
A71: c2,b1 _|_ a2,a1 by A1, CONAFFM:def 3;
reconsider c2' = c2 as Element of by ANALMETR:47;
a1,b1 _|_ c1,a2 by A9, A11, A18, A50, ANALMETR:84;
then c2,a2 // c1,a2 by A69, A62, ANALMETR:85;
then a2,c1 // a2,c2 by ANALMETR:81;
then A72: a2',c1' // a2',c2' by ANALMETR:48;
a2,a1 _|_ b1,b2 by A3, A4, A7, A8, A12, ANALMETR:78;
then b1,b2 // c2,b1 by A64, A71, ANALMETR:85;
then b1,b2 // b1,c2 by ANALMETR:81;
then LIN b1,b2,c2 by ANALMETR:def 11;
then LIN b1',b2',c2' by ANALMETR:55;
then A73: c2' in N' by A7, A8, A19, A42, AFF_1:39;
A74: not LIN o',a1',c2'

proof

A75: o' <> c2'

proof

A76: a2 <> b1

proof

o',b1' // o',b2' by A6, A7, A8, A19, AFF_1:53, AFF_1:55;
then A77: LIN o',b1',b2' by AFF_1:def 1;
assume a2 = b1 ; :: thesis: contradiction
hence contradiction by A2, A4, A10, A14, A20, A77, AFF_1:39; :: thesis: verum

end;

assume o' = c2' ; :: thesis: contradiction
then A78: o,a1 _|_ a3,b2 by A17, A70, A76, ANALMETR:84;
o,a1 _|_ b3,b2 by A2, A3, A8, A9, A12, ANALMETR:78;
then b3,b2 // a3,b2 by A13, A78, ANALMETR:85;
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 A8, A9, A11, A19, A38, AFF_1:39; :: thesis: verum

end;

o',a1' // o',a3' by A2, A3, A5, A20, AFF_1:53, AFF_1:55;
then A79: LIN o',a1',a3' by AFF_1:def 1;
assume LIN o',a1',c2' ; :: thesis: contradiction
then LIN o',c2',a1' by AFF_1:15;
then a1' in N' by A6, A19, A73, A75, AFF_1:39;
hence contradiction by A6, A11, A13, A19, A79, AFF_1:39; :: thesis: verum

end;

not LIN a3,a1,b2

proof

assume LIN a3,a1,b2 ; :: thesis: contradiction
then LIN a3',a1',b2' by ANALMETR:55;
hence contradiction by A3, A5, A10, A20, A37, AFF_1:39; :: thesis: verum

end;

then consider c3 being Element of such that
A80: c3,a3 _|_ a1,b2 and
A81: c3,a1 _|_ a3,b2 and
A82: c3,b2 _|_ a3,a1 by A1, CONAFFM:def 3;
reconsider c3' = c3 as Element of by ANALMETR:47;
a2 <> b1

proof

o',b1' // o',b2' by A6, A7, A8, A19, AFF_1:53, AFF_1:55;
then A83: LIN o',b1',b2' by AFF_1:def 1;
assume a2 = b1 ; :: thesis: contradiction
hence contradiction by A2, A4, A10, A14, A20, A83, AFF_1:39; :: thesis: verum

end;

then a3,b2 _|_ c2,a1 by A17, A70, ANALMETR:84;
then c2,a1 // c3,a1 by A5, A10, A81, ANALMETR:85;
then a1,c2 // a1,c3 by ANALMETR:81;
then A84: a1',c2' // a1',c3' by ANALMETR:48;
a2,a1 _|_ b2,b1 by A3, A4, A7, A8, A12, ANALMETR:78;
then b2,b1 // c2,b1 by A64, A71, ANALMETR:85;
then b1,b2 // b1,c2 by ANALMETR:81;
then LIN b1,b2,c2 by ANALMETR:def 11;
then LIN b1',b2',c2' by ANALMETR:55;
then c2 in N by A7, A8, A19, A42, AFF_1:39;
then o',c1' // o',c2' by A6, A19, A57, AFF_1:53, AFF_1:55;
then LIN o',c1',c2' by AFF_1:def 1;
then A85: c1 = c2 by A58, A72, AFF_1:23;
A86: c1 <> a3

proof

A87: a2 <> a3

proof

A88: not LIN o',a3',b1'

proof

assume LIN o',a3',b1' ; :: thesis: contradiction
then LIN o',b1',a3' by AFF_1:15;
hence contradiction by A6, A7, A11, A15, A19, AFF_1:39; :: thesis: verum

end;

assume a2 = a3 ; :: thesis: contradiction
then a3',b2' // a3',b1' by A17, ANALMETR:48;
then A89: a3',b1' // a3',b2' by AFF_1:13;
o',b1' // o',b2' by A6, A7, A8, A19, AFF_1:53, AFF_1:55;
then LIN o',b1',b2' by AFF_1:def 1;
hence contradiction by A42, A88, A89, AFF_1:23; :: thesis: verum

end;

assume A90: c1 = a3 ; :: thesis: contradiction
a2,a3 _|_ b2,b3 by A4, A5, A8, A9, A12, ANALMETR:78;
then a3,b3 // b2,b3 by A52, A90, A87, ANALMETR:85;
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 A8, A9, A11, A19, A38, AFF_1:39; :: thesis: verum

end;

a3,a1 _|_ b2,b3 by A3, A5, A8, A9, A12, ANALMETR:78;
then c3,b2 // b2,b3 by A37, A82, ANALMETR:85;
then b2,b3 // b2,c3 by ANALMETR:81;
then LIN b2,b3,c3 by ANALMETR:def 11;
then LIN b2',b3',c3' by ANALMETR:55;
then c3' in N' by A8, A9, A19, A38, AFF_1:39;
then o',c2' // o',c3' by A6, A19, A73, AFF_1:53, AFF_1:55;
then LIN o',c2',c3' by AFF_1:def 1;
then c2 = c3 by A74, A84, AFF_1:23;
hence a1,b2 // a2,b3 by A51, A85, A80, A86, ANALMETR:85; :: thesis: verum

end;

now

o',b2' // o',b3' by A6, A8, A9, A19, AFF_1:53, AFF_1:55;
then A91: LIN o',b2',b3' by AFF_1:def 1;
assume A92: a2 = a1 ; :: thesis: a1,b2 // a2,b3
a1 <> b1

proof

o',b1' // o',b2' by A6, A7, A8, A19, AFF_1:53, AFF_1:55;
then A93: LIN o',b1',b2' by AFF_1:def 1;
assume a1 = b1 ; :: thesis: contradiction
hence contradiction by A2, A3, A10, A13, A20, A93, AFF_1:39; :: thesis: verum

end;

then a3,b2 // a3,b3 by A17, A18, A92, ANALMETR:82;
then a3',b2' // a3',b3' by ANALMETR:48;
then b2' = b3' by A2, A5, A6, A10, A11, A20, A91, AFF_1:23, AFF_1:39;
then a1',b2' // a2',b3' by A92, AFF_1:11;
hence a1,b2 // a2,b3 by ANALMETR:48; :: thesis: verum

end;

hence a1,b2 // a2,b3 by A53; :: thesis: verum

end;

now

A94: not LIN o',b2',a3'

proof

assume LIN o',b2',a3' ; :: thesis: contradiction
then LIN o,b2,a3 by ANALMETR:55;
then LIN b2,o,a3 by A27;
then A95: b2,o // b2,a3 by ANALMETR:def 11;
LIN b2,o,b3 by A27, A36;
then b2,o // b2,b3 by ANALMETR:def 11;
then b2,a3 // b2,b3 by A2, A10, A95, ANALMETR:82;
hence contradiction by A39, ANALMETR:def 11; :: thesis: verum

end;

LIN a3,a1,o by A27, A34;
then A96: a3,a1 // a3,o by ANALMETR:def 11;
A97: a3 <> a1

proof

assume a3 = a1 ; :: thesis: contradiction
then LIN a3',a1',b2' by AFF_1:16;
hence contradiction by A39, ANALMETR:55; :: thesis: verum

end;

a3,a1 // a3,a2 by A35, ANALMETR:def 11;
then a3,o // a3,a2 by A96, A97, ANALMETR:82;
then LIN a3,o,a2 by ANALMETR:def 11;
then LIN o,a3,a2 by A27;
then A98: LIN o',a3',a2' by ANALMETR:55;
assume A99: b2 = b1 ; :: thesis: a1,b2 // a2,b3
then b2,a3 // b2,a2 by A17, ANALMETR:81;
then b2',a3' // b2',a2' by ANALMETR:48;
then a3' = a2' by A98, A94, AFF_1:23;
hence a1,b2 // a2,b3 by A18, A99, ANALMETR:81; :: thesis: verum

end;

hence a1,b2 // a2,b3 by A41; :: thesis: verum

end;

now

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

proof

o',b1' // o',b2' by A6, A7, A8, A19, AFF_1:53, AFF_1:55;
then A101: LIN o',b1',b2' by AFF_1:def 1;
assume LIN o',a1',b1' ; :: thesis: contradiction
then b1' in M' by A2, A3, A13, A20, AFF_1:39;
hence contradiction by A2, A10, A15, A20, A101, AFF_1:39; :: thesis: verum

end;

o',b1' // o',b3' by A6, A7, A9, A19, AFF_1:53, AFF_1:55;
then A102: LIN o',b1',b3' by AFF_1:def 1;
assume A103: a1 = a3 ; :: thesis: a1,b2 // a2,b3
then a1,b1 // a1,b3 by A18, ANALMETR:81;
then a1',b1' // a1',b3' by ANALMETR:48;
hence a1,b2 // a2,b3 by A17, A103, A100, A102, AFF_1:23; :: thesis: verum

end;

hence a1,b2 // a2,b3 by A21, A33; :: thesis: verum