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 X; :: according to CONMETR:def 1 :: thesis: for a1, a2, a3, b1, b2, b3 being Element of X
for M, N being Subset of X 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 X; :: thesis: for M, N being Subset of X 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 X; :: 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 A2: ( 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 ) ; :: thesis: a1,b2 // a2,b3
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;
( M is being_line & N is being_line ) by A2, ANALMETR:62;
then A3: ( M' is being_line & N' is being_line ) by ANALMETR:58;
then A4: ( M' // M' & N' // N' ) by AFF_1:55;
A5: for a, b, c being Element of X 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 X; :: 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 ) )
assume A6: 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 )
reconsider a' = a, b' = b, c' = c as Element of (Af X) by ANALMETR:47;
LIN a',b',c' by A6, ANALMETR:55;
then ( LIN a',c',b' & LIN b',a',c' & LIN b',c',a' & LIN c',a',b' & LIN c',b',a' ) by 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 ANALMETR:55; :: thesis: verum

end;

A7: now

assume A8: a1 = a3 ; :: thesis: a1,b2 // a2,b3
A9: not LIN o',a1',b1'

proof

assume LIN o',a1',b1' ; :: thesis: contradiction
then A10: b1' in M' by A2, A3, AFF_1:39;
o',b1' // o',b2' by A2, A4, AFF_1:53;
then LIN o',b1',b2' by AFF_1:def 1;
hence contradiction by A2, A3, A10, AFF_1:39; :: thesis: verum

end;

A11: LIN o',b1',b3'

proof

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

end;

a1',b1' // a1',b3'

proof

a1,b1 // a1,b3 by A2, A8, ANALMETR:81;
hence a1',b1' // a1',b3' by ANALMETR:48; :: thesis: verum

end;

hence a1,b2 // a2,b3 by A2, A8, A9, A11, AFF_1:23; :: thesis: verum

end;

A12: now

assume A13: b2 = b3 ; :: thesis: a1,b2 // a2,b3
A14: not LIN o',b1',a1'

proof

assume LIN o',b1',a1' ; :: thesis: contradiction
then A15: a1' in N' by A2, A3, AFF_1:39;
o',a1' // o',a3' by A2, A4, AFF_1:53;
then LIN o',a1',a3' by AFF_1:def 1;
hence contradiction by A2, A3, A15, AFF_1:39; :: thesis: verum

end;

A16: LIN o',a1',a2'

proof

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

end;

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

proof

A17: b1,a1 // a3,b2 by A2, A13, ANALMETR:81;
b1,a2 // a3,b2 by A2, ANALMETR:81;
then b1,a1 // b1,a2 by A2, A17, ANALMETR:82;
hence b1',a1' // b1',a2' by ANALMETR:48; :: thesis: verum

end;

then a1' = a2' by A14, A16, AFF_1:23;
then a1',b2' // a2',b3' by A13, AFF_1:11;
hence a1,b2 // a2,b3 by ANALMETR:48; :: thesis: verum

end;

now

assume A18: ( a1 <> a3 & b2 <> b3 ) ; :: thesis: a1,b2 // a2,b3
A19: ( LIN o,a3,a1 & LIN a3,a1,a2 & LIN o,b2,b3 & LIN b2,b3,b1 & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & not LIN a3,a1,b2 & not LIN b2,a3,b3 & o,a3 _|_ o,b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 )

proof

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

proof

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

end;

( 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 A2, A3, A18, AFF_1:39; :: thesis: verum

end;

hence ( LIN o,a3,a1 & LIN a3,a1,a2 & LIN o,b2,b3 & LIN b2,b3,b1 & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & not LIN a3,a1,b2 & not LIN b2,a3,b3 & o,a3 _|_ o,b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 ) by A2, A20, ANALMETR:78; :: thesis: verum

end;

A21: now

assume A22: b2 = b1 ; :: thesis: a1,b2 // a2,b3
then b2,a3 // b2,a2 by A19, ANALMETR:81;
then A23: b2',a3' // b2',a2' by ANALMETR:48;
LIN a3,a1,o by A5, A19;
then A24: a3,a1 // a3,o by ANALMETR:def 11;
A25: a3 <> a1

proof

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

end;

a3,a1 // a3,a2 by A19, ANALMETR:def 11;
then a3,o // a3,a2 by A24, A25, ANALMETR:82;
then LIN a3,o,a2 by ANALMETR:def 11;
then LIN o,a3,a2 by A5;
then A26: LIN o',a3',a2' by ANALMETR:55;
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 A5;
then A27: b2,o // b2,a3 by ANALMETR:def 11;
LIN b2,o,b3 by A5, A19;
then b2,o // b2,b3 by ANALMETR:def 11;
then b2,a3 // b2,b3 by A19, A27, ANALMETR:82;
hence contradiction by A19, ANALMETR:def 11; :: thesis: verum

end;

then a3' = a2' by A23, A26, AFF_1:23;
hence a1,b2 // a2,b3 by A19, A22, ANALMETR:81; :: thesis: verum

end;

now

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

proof

assume LIN a2,a3,b3 ; :: thesis: contradiction
then LIN a3,a2,b3 by A5;
then A29: a3,a2 // a3,b3 by ANALMETR:def 11;
A30: a3 <> a2

proof

assume a3 = a2 ; :: thesis: contradiction
then LIN a3,b2,b1 by A19, ANALMETR:def 11;
then LIN b2,b1,a3 by A5;
then A31: b2,b1 // b2,a3 by ANALMETR:def 11;
LIN b2,b1,b3 by A5, A19;
then b2,b1 // b2,b3 by ANALMETR:def 11;
then b2,a3 // b2,b3 by A28, A31, ANALMETR:82;
hence contradiction by A19, ANALMETR:def 11; :: thesis: verum

end;

LIN a3,a2,a1 by A5, A19;
then a3,a2 // a3,a1 by ANALMETR:def 11;
then A32: a3,a1 // a3,b3 by A29, A30, ANALMETR:82;
A33: a3 <> a1

proof

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

end;

LIN a3,a1,o by A5, A19;
then a3,a1 // a3,o by ANALMETR:def 11;
then a3,o // a3,b3 by A32, A33, ANALMETR:82;
then a3',o' // a3',b3' by ANALMETR:48;
then A34: a3',b3' // a3',o' by AFF_1:13;
A35: not LIN b2',a3',b3' by A19, ANALMETR:55;
LIN b2,b3,o by A5, A19;
then LIN b2',b3',o' by ANALMETR:55;
hence contradiction by A19, A34, A35, AFF_1:23; :: thesis: verum

end;

then consider c1 being Element of X such that
A36: ( c1,a2 _|_ a3,b3 & c1,a3 _|_ a2,b3 & c1,b3 _|_ a2,a3 ) by A1, CONAFFM:def 3;
reconsider c1' = c1 as Element of (Af X) by ANALMETR:47;

A37: now

assume A38: a2 = a1 ; :: thesis: a1,b2 // a2,b3
A39: not LIN o',a3',b2' by A2, A3, AFF_1:39;
A40: LIN o',b2',b3'

proof

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

end;

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

proof

a1 <> b1

proof

assume A41: a1 = b1 ; :: thesis: contradiction
o',b1' // o',b2' by A2, A4, AFF_1:53;
then LIN o',b1',b2' by AFF_1:def 1;
hence contradiction by A2, A3, A41, AFF_1:39; :: thesis: verum

end;

then a3,b2 // a3,b3 by A2, A38, ANALMETR:82;
hence a3',b2' // a3',b3' by ANALMETR:48; :: thesis: verum

end;

then b2' = b3' by A39, A40, AFF_1:23;
then a1',b2' // a2',b3' by A38, AFF_1:11;
hence a1,b2 // a2,b3 by ANALMETR:48; :: thesis: verum

end;

now

assume A42: a2 <> a1 ; :: thesis: a1,b2 // a2,b3
A43: a1 <> b1

proof

assume A44: a1 = b1 ; :: thesis: contradiction
LIN a1,a2,a3 by A5, A19;
then a1,a2 // a1,a3 by ANALMETR:def 11;
then a2,a1 // a3,a1 by ANALMETR:81;
then a3,a1 // a3,b2 by A19, A42, A44, ANALMETR:82;
hence contradiction by A19, 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 A5;
then b1,a1 // b1,a2 by ANALMETR:def 11;
then A45: a1,b1 // a2,b1 by ANALMETR:81;
A46: a2 <> b1

proof

assume A47: a2 = b1 ; :: thesis: contradiction
o',b1' // o',b2' by A2, A4, AFF_1:53;
then LIN o',b1',b2' by AFF_1:def 1;
hence contradiction by A2, A3, A47, AFF_1:39; :: thesis: verum

end;

a2,b1 // a3,b3 by A19, A43, A45, ANALMETR:82;
then a3,b3 // a3,b2 by A19, A46, ANALMETR:82;
then LIN a3,b3,b2 by ANALMETR:def 11;
hence contradiction by A5, A19; :: thesis: verum

end;

then consider c2 being Element of X such that
A48: ( c2,a2 _|_ a1,b1 & c2,a1 _|_ a2,b1 & c2,b1 _|_ a2,a1 ) by A1, CONAFFM:def 3;
reconsider c2' = c2 as Element of (Af X) by ANALMETR:47;
A49: c1 = c2

proof

A50: ( c1 in N & c2 in N )

proof

A51: a2,a3 _|_ b2,b3 by A2, ANALMETR:78;
a2 <> a3

proof

assume A52: a2 = a3 ; :: thesis: contradiction
A53: 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 A2, A3, AFF_1:39; :: thesis: verum

end;

A54: LIN o',b1',b2'

proof

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

end;

a3',b1' // a3',b2'

proof

a3',b2' // a3',b1' by A2, A52, ANALMETR:48;
hence a3',b1' // a3',b2' by AFF_1:13; :: thesis: verum

end;

hence contradiction by A28, A53, A54, AFF_1:23; :: thesis: verum

end;

then b2,b3 // c1,b3 by A36, A51, ANALMETR:85;
then b3,b2 // b3,c1 by ANALMETR:81;
then LIN b3,b2,c1 by ANALMETR:def 11;
then A55: LIN b3',b2',c1' by ANALMETR:55;
a2,a1 _|_ b2,b1 by A2, ANALMETR:78;
then b2,b1 // c2,b1 by A42, A48, 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;
hence ( c1 in N & c2 in N ) by A2, A3, A18, A28, A55, AFF_1:39; :: thesis: verum

end;

then o',c1' // o',c2' by A2, A4, AFF_1:53;
then A56: LIN o',c1',c2' by AFF_1:def 1;
A57: not LIN o',a2',c1'

proof

assume LIN o',a2',c1' ; :: thesis: contradiction
then A58: LIN o',c1',a2' by AFF_1:15;
o' <> c1'

proof

assume A59: o' = c1' ; :: thesis: contradiction
o,a2 _|_ b3,b2 by A2, ANALMETR:78;
then b3,b2 // a3,b3 by A2, A36, A59, 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 A2, A3, A18, AFF_1:39; :: thesis: verum

end;

then A60: a2' in N' by A2, A3, A50, A58, AFF_1:39;
o',a2' // o',a3' by A2, A4, AFF_1:53;
then LIN o',a2',a3' by AFF_1:def 1;
hence contradiction by A2, A3, A60, AFF_1:39; :: thesis: verum

end;

a2',c1' // a2',c2'

proof

A61: a1 <> b1

proof

assume A62: a1 = b1 ; :: thesis: contradiction
o',b1' // o',b2' by A2, A4, AFF_1:53;
then LIN o',b1',b2' by AFF_1:def 1;
hence contradiction by A2, A3, A62, AFF_1:39; :: thesis: verum

end;

a1,b1 _|_ c1,a2 by A2, A36, ANALMETR:84;
then c2,a2 // c1,a2 by A48, A61, ANALMETR:85;
then a2,c1 // a2,c2 by ANALMETR:81;
hence a2',c1' // a2',c2' by ANALMETR:48; :: thesis: verum

end;

hence c1 = c2 by A56, A57, AFF_1:23; :: 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 A2, A3, A18, AFF_1:39; :: thesis: verum

end;

then consider c3 being Element of X such that
A63: ( c3,a3 _|_ a1,b2 & c3,a1 _|_ a3,b2 & c3,b2 _|_ a3,a1 ) by A1, CONAFFM:def 3;
reconsider c3' = c3 as Element of (Af X) by ANALMETR:47;
A64: c2 = c3

proof

A65: ( c2' in N' & c3' in N' )

proof

a2,a1 _|_ b1,b2 by A2, ANALMETR:78;
then b1,b2 // c2,b1 by A42, A48, ANALMETR:85;
then b1,b2 // b1,c2 by ANALMETR:81;
then LIN b1,b2,c2 by ANALMETR:def 11;
then A66: LIN b1',b2',c2' by ANALMETR:55;
a3,a1 _|_ b2,b3 by A2, ANALMETR:78;
then c3,b2 // b2,b3 by A18, A63, 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;
hence ( c2' in N' & c3' in N' ) by A2, A3, A18, A28, A66, AFF_1:39; :: thesis: verum

end;

A67: LIN o',c2',c3'

proof

o',c2' // o',c3' by A2, A4, A65, AFF_1:53;
hence LIN o',c2',c3' by AFF_1:def 1; :: thesis: verum

end;

A68: not LIN o',a1',c2'

proof

assume A69: LIN o',a1',c2' ; :: thesis: contradiction
A70: o' <> c2'

proof

assume A71: o' = c2' ; :: thesis: contradiction
A72: a2 <> b1

proof

assume A73: a2 = b1 ; :: thesis: contradiction
o',b1' // o',b2' by A2, A4, AFF_1:53;
then LIN o',b1',b2' by AFF_1:def 1;
hence contradiction by A2, A3, A73, AFF_1:39; :: thesis: verum

end;

A74: o,a1 _|_ b3,b2 by A2, ANALMETR:78;
o,a1 _|_ a3,b2 by A2, A48, A71, A72, ANALMETR:84;
then b3,b2 // a3,b2 by A2, A74, 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 A2, A3, A18, AFF_1:39; :: thesis: verum

end;

LIN o',c2',a1' by A69, AFF_1:15;
then A75: a1' in N' by A2, A3, A65, A70, AFF_1:39;
o',a1' // o',a3' by A2, A4, AFF_1:53;
then LIN o',a1',a3' by AFF_1:def 1;
hence contradiction by A2, A3, A75, AFF_1:39; :: thesis: verum

end;

a1',c2' // a1',c3'

proof

a2 <> b1

proof

assume A76: a2 = b1 ; :: thesis: contradiction
o',b1' // o',b2' by A2, A4, AFF_1:53;
then LIN o',b1',b2' by AFF_1:def 1;
hence contradiction by A2, A3, A76, AFF_1:39; :: thesis: verum

end;

then a3,b2 _|_ c2,a1 by A2, A48, ANALMETR:84;
then c2,a1 // c3,a1 by A2, A63, ANALMETR:85;
then a1,c2 // a1,c3 by ANALMETR:81;
hence a1',c2' // a1',c3' by ANALMETR:48; :: thesis: verum

end;

hence c2 = c3 by A67, A68, AFF_1:23; :: thesis: verum

end;

c1 <> a3

proof

assume A77: c1 = a3 ; :: thesis: contradiction
A78: a2,a3 _|_ b2,b3 by A2, ANALMETR:78;
a2 <> a3

proof

assume A79: a2 = a3 ; :: thesis: contradiction
A80: 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 A2, A3, AFF_1:39; :: thesis: verum

end;

A81: LIN o',b1',b2'

proof

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

end;

a3',b1' // a3',b2'

proof

a3',b2' // a3',b1' by A2, A79, ANALMETR:48;
hence a3',b1' // a3',b2' by AFF_1:13; :: thesis: verum

end;

hence contradiction by A28, A80, A81, AFF_1:23; :: thesis: verum

end;

then a3,b3 // b2,b3 by A36, A77, A78, 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 A2, A3, A18, AFF_1:39; :: thesis: verum

end;

hence a1,b2 // a2,b3 by A36, A49, A63, A64, ANALMETR:85; :: thesis: verum

end;

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

end;

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

end;

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