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 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 o9 = o, a19 = a1, a29 = a2, a39 = a3, b19 = b1, b29 = b2, b39 = b3 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
reconsider M9 = M, N9 = N as Subset of AffinStruct(# the carrier of X, the CONGR of X #) ;
N is being_line by A12, ANALMETR:44;
then A19: N9 is being_line by ANALMETR:43;
M is being_line by A12, ANALMETR:44;
then A20: M9 is being_line by ANALMETR:43;
A21: now :: thesis: ( b2 = b3 implies a1,b2 // a2,b3 )
A22: not LIN o9,b19,a19
proof
o9,a19 // o9,a39 by A2, A3, A5, A20, AFF_1:39, AFF_1:41;
then A23: LIN o9,a19,a39 by AFF_1:def 1;
assume LIN o9,b19,a19 ; :: thesis: contradiction
then a19 in N9 by A6, A7, A15, A19, AFF_1:25;
hence contradiction by A6, A11, A13, A19, A23, AFF_1:25; :: thesis: verum
end;
A24: b1,a2 // a3,b2 by A17, ANALMETR:59;
o9,a19 // o9,a29 by A2, A3, A4, A20, AFF_1:39, AFF_1:41;
then A25: LIN o9,a19,a29 by AFF_1:def 1;
assume A26: b2 = b3 ; :: thesis: a1,b2 // a2,b3
then b1,a1 // a3,b2 by A18, ANALMETR:59;
then b1,a1 // b1,a2 by A5, A10, A24, ANALMETR:60;
then b19,a19 // b19,a29 by ANALMETR:36;
then a19 = a29 by A22, A25, AFF_1:14;
then a19,b29 // a29,b39 by A26, AFF_1:2;
hence a1,b2 // a2,b3 by ANALMETR:36; :: thesis: verum
end;
A27: 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 ) )
reconsider a9 = a, b9 = b, c9 = c as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
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 a9,b9,c9 by ANALMETR:40;
then A29: LIN b9,a9,c9 by AFF_1:6;
A30: LIN c9,a9,b9 by A28, AFF_1:6;
A31: LIN b9,c9,a9 by A28, AFF_1:6;
A32: LIN c9,b9,a9 by A28, AFF_1:6;
LIN a9,c9,b9 by A28, AFF_1:6;
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:40; :: thesis: verum
end;
A33: now :: thesis: ( a1 <> a3 & b2 <> b3 implies a1,b2 // a2,b3 )
o9,a39 // o9,a19 by A2, A3, A5, A20, AFF_1:39, AFF_1:41;
then LIN o9,a39,a19 by AFF_1:def 1;
then A34: LIN o,a3,a1 by ANALMETR:40;
a39,a19 // a39,a29 by A3, A4, A5, A20, AFF_1:39, AFF_1:41;
then LIN a39,a19,a29 by AFF_1:def 1;
then A35: LIN a3,a1,a2 by ANALMETR:40;
o9,b29 // o9,b39 by A6, A8, A9, A19, AFF_1:39, AFF_1:41;
then LIN o9,b29,b39 by AFF_1:def 1;
then A36: LIN o,b2,b3 by ANALMETR:40;
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 a39,a19,b29 or LIN b29,a39,b39 ) by ANALMETR:40;
then ( LIN a39,a19,b29 or LIN b29,b39,a39 ) by AFF_1:6;
hence contradiction by A3, A5, A8, A9, A10, A11, A20, A19, A37, A38, AFF_1:25; :: thesis: verum
end;
b29,b39 // b29,b19 by A7, A8, A9, A19, AFF_1:39, AFF_1:41;
then LIN b29,b39,b19 by AFF_1:def 1;
then A40: LIN b2,b3,b1 by ANALMETR:40;
A41: now :: thesis: ( b2 <> b1 implies a1,b2 // a2,b3 )
assume A42: b2 <> b1 ; :: thesis: a1,b2 // a2,b3
not LIN a2,a3,b3
proof
A43: a3 <> a2 LIN a3,a1,o by A27, A34;
then A45: a3,a1 // a3,o by ANALMETR:def 10;
A46: a3 <> a1
proof
assume a3 = a1 ; :: thesis: contradiction
then LIN a39,a19,b29 by AFF_1:7;
hence contradiction by A39, ANALMETR:40; :: 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 10;
LIN a3,a2,a1 by A27, A35;
then a3,a2 // a3,a1 by ANALMETR:def 10;
then a3,a1 // a3,b3 by A47, A43, ANALMETR:60;
then a3,o // a3,b3 by A46, A45, ANALMETR:60;
then a39,o9 // a39,b39 by ANALMETR:36;
then A48: a39,b39 // a39,o9 by AFF_1:4;
LIN b2,b3,o by A27, A36;
then A49: LIN b29,b39,o9 by ANALMETR:40;
not LIN b29,a39,b39 by A39, ANALMETR:40;
hence contradiction by A16, A48, A49, AFF_1:14; :: thesis: verum
end;
then consider c1 being Element of X 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 c19 = c1 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
A53: now :: thesis: ( a2 <> a1 implies a1,b2 // a2,b3 )
A54: a2 <> a3
proof
A55: not LIN o9,a39,b19
proof
assume LIN o9,a39,b19 ; :: thesis: contradiction
then LIN o9,b19,a39 by AFF_1:6;
hence contradiction by A6, A7, A11, A15, A19, AFF_1:25; :: thesis: verum
end;
assume a2 = a3 ; :: thesis: contradiction
then a39,b29 // a39,b19 by A17, ANALMETR:36;
then A56: a39,b19 // a39,b29 by AFF_1:4;
o9,b19 // o9,b29 by A6, A7, A8, A19, AFF_1:39, AFF_1:41;
then LIN o9,b19,b29 by AFF_1:def 1;
hence contradiction by A42, A55, A56, AFF_1:14; :: thesis: verum
end;
a2,a3 _|_ b2,b3 by A4, A5, A8, A9, A12, ANALMETR:56;
then b2,b3 // c1,b3 by A52, A54, ANALMETR:63;
then b3,b2 // b3,c1 by ANALMETR:59;
then LIN b3,b2,c1 by ANALMETR:def 10;
then LIN b39,b29,c19 by ANALMETR:40;
then A57: c1 in N by A8, A9, A19, A38, AFF_1:25;
A58: not LIN o9,a29,c19
proof
A59: o9 <> c19
proof
assume A60: o9 = c19 ; :: thesis: contradiction
o,a2 _|_ b3,b2 by A2, A4, A8, A9, A12, ANALMETR:56;
then b3,b2 // a3,b3 by A14, A50, A60, ANALMETR:63;
then b3,b2 // b3,a3 by ANALMETR:59;
then LIN b3,b2,a3 by ANALMETR:def 10;
then LIN b39,b29,a39 by ANALMETR:40;
hence contradiction by A8, A9, A11, A19, A38, AFF_1:25; :: thesis: verum
end;
o9,a29 // o9,a39 by A2, A4, A5, A20, AFF_1:39, AFF_1:41;
then A61: LIN o9,a29,a39 by AFF_1:def 1;
assume LIN o9,a29,c19 ; :: thesis: contradiction
then LIN o9,c19,a29 by AFF_1:6;
then a29 in N9 by A6, A19, A57, A59, AFF_1:25;
hence contradiction by A6, A11, A14, A19, A61, AFF_1:25; :: thesis: verum
end;
A62: a1 <> b1
proof
o9,b19 // o9,b29 by A6, A7, A8, A19, AFF_1:39, AFF_1:41;
then A63: LIN o9,b19,b29 by AFF_1:def 1;
assume a1 = b1 ; :: thesis: contradiction
hence contradiction by A2, A3, A10, A13, A20, A63, AFF_1:25; :: thesis: verum
end;
assume A64: a2 <> a1 ; :: thesis: a1,b2 // a2,b3
A65: a1 <> b1 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 10;
then a1,b1 // a2,b1 by ANALMETR:59;
then A67: a2,b1 // a3,b3 by A18, A65, ANALMETR:60;
a2 <> b1
proof
o9,b19 // o9,b29 by A6, A7, A8, A19, AFF_1:39, AFF_1:41;
then A68: LIN o9,b19,b29 by AFF_1:def 1;
assume a2 = b1 ; :: thesis: contradiction
hence contradiction by A2, A4, A10, A14, A20, A68, AFF_1:25; :: thesis: verum
end;
then a3,b3 // a3,b2 by A17, A67, ANALMETR:60;
then LIN a3,b3,b2 by ANALMETR:def 10;
hence contradiction by A27, A39; :: thesis: verum
end;
then consider c2 being Element of X 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 c29 = c2 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
a1,b1 _|_ c1,a2 by A9, A11, A18, A50, ANALMETR:62;
then c2,a2 // c1,a2 by A69, A62, ANALMETR:63;
then a2,c1 // a2,c2 by ANALMETR:59;
then A72: a29,c19 // a29,c29 by ANALMETR:36;
a2,a1 _|_ b1,b2 by A3, A4, A7, A8, A12, ANALMETR:56;
then b1,b2 // c2,b1 by A64, A71, ANALMETR:63;
then b1,b2 // b1,c2 by ANALMETR:59;
then LIN b1,b2,c2 by ANALMETR:def 10;
then LIN b19,b29,c29 by ANALMETR:40;
then A73: c29 in N9 by A7, A8, A19, A42, AFF_1:25;
A74: not LIN o9,a19,c29
proof
A75: o9 <> c29 o9,a19 // o9,a39 by A2, A3, A5, A20, AFF_1:39, AFF_1:41;
then A79: LIN o9,a19,a39 by AFF_1:def 1;
assume LIN o9,a19,c29 ; :: thesis: contradiction
then LIN o9,c29,a19 by AFF_1:6;
then a19 in N9 by A6, A19, A73, A75, AFF_1:25;
hence contradiction by A6, A11, A13, A19, A79, AFF_1:25; :: thesis: verum
end;
not LIN a3,a1,b2
proof
assume LIN a3,a1,b2 ; :: thesis: contradiction
then LIN a39,a19,b29 by ANALMETR:40;
hence contradiction by A3, A5, A10, A20, A37, AFF_1:25; :: thesis: verum
end;
then consider c3 being Element of X 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 c39 = c3 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
a2 <> b1
proof
o9,b19 // o9,b29 by A6, A7, A8, A19, AFF_1:39, AFF_1:41;
then A83: LIN o9,b19,b29 by AFF_1:def 1;
assume a2 = b1 ; :: thesis: contradiction
hence contradiction by A2, A4, A10, A14, A20, A83, AFF_1:25; :: thesis: verum
end;
then a3,b2 _|_ c2,a1 by A17, A70, ANALMETR:62;
then c2,a1 // c3,a1 by A5, A10, A81, ANALMETR:63;
then a1,c2 // a1,c3 by ANALMETR:59;
then A84: a19,c29 // a19,c39 by ANALMETR:36;
a2,a1 _|_ b2,b1 by A3, A4, A7, A8, A12, ANALMETR:56;
then b2,b1 // c2,b1 by A64, A71, ANALMETR:63;
then b1,b2 // b1,c2 by ANALMETR:59;
then LIN b1,b2,c2 by ANALMETR:def 10;
then LIN b19,b29,c29 by ANALMETR:40;
then c2 in N by A7, A8, A19, A42, AFF_1:25;
then o9,c19 // o9,c29 by A6, A19, A57, AFF_1:39, AFF_1:41;
then LIN o9,c19,c29 by AFF_1:def 1;
then A85: c1 = c2 by A58, A72, AFF_1:14;
A86: c1 <> a3
proof
A87: a2 <> a3
proof
A88: not LIN o9,a39,b19
proof
assume LIN o9,a39,b19 ; :: thesis: contradiction
then LIN o9,b19,a39 by AFF_1:6;
hence contradiction by A6, A7, A11, A15, A19, AFF_1:25; :: thesis: verum
end;
assume a2 = a3 ; :: thesis: contradiction
then a39,b29 // a39,b19 by A17, ANALMETR:36;
then A89: a39,b19 // a39,b29 by AFF_1:4;
o9,b19 // o9,b29 by A6, A7, A8, A19, AFF_1:39, AFF_1:41;
then LIN o9,b19,b29 by AFF_1:def 1;
hence contradiction by A42, A88, A89, AFF_1:14; :: thesis: verum
end;
assume A90: c1 = a3 ; :: thesis: contradiction
a2,a3 _|_ b2,b3 by A4, A5, A8, A9, A12, ANALMETR:56;
then a3,b3 // b2,b3 by A52, A90, A87, ANALMETR:63;
then b3,b2 // b3,a3 by ANALMETR:59;
then LIN b3,b2,a3 by ANALMETR:def 10;
then LIN b39,b29,a39 by ANALMETR:40;
hence contradiction by A8, A9, A11, A19, A38, AFF_1:25; :: thesis: verum
end;
a3,a1 _|_ b2,b3 by A3, A5, A8, A9, A12, ANALMETR:56;
then c3,b2 // b2,b3 by A37, A82, ANALMETR:63;
then b2,b3 // b2,c3 by ANALMETR:59;
then LIN b2,b3,c3 by ANALMETR:def 10;
then LIN b29,b39,c39 by ANALMETR:40;
then c39 in N9 by A8, A9, A19, A38, AFF_1:25;
then o9,c29 // o9,c39 by A6, A19, A73, AFF_1:39, AFF_1:41;
then LIN o9,c29,c39 by AFF_1:def 1;
then c2 = c3 by A74, A84, AFF_1:14;
hence a1,b2 // a2,b3 by A51, A85, A80, A86, ANALMETR:63; :: thesis: verum
end;
now :: thesis: ( a2 = a1 implies a1,b2 // a2,b3 )
o9,b29 // o9,b39 by A6, A8, A9, A19, AFF_1:39, AFF_1:41;
then A91: LIN o9,b29,b39 by AFF_1:def 1;
assume A92: a2 = a1 ; :: thesis: a1,b2 // a2,b3
a1 <> b1
proof
o9,b19 // o9,b29 by A6, A7, A8, A19, AFF_1:39, AFF_1:41;
then A93: LIN o9,b19,b29 by AFF_1:def 1;
assume a1 = b1 ; :: thesis: contradiction
hence contradiction by A2, A3, A10, A13, A20, A93, AFF_1:25; :: thesis: verum
end;
then a3,b2 // a3,b3 by A17, A18, A92, ANALMETR:60;
then a39,b29 // a39,b39 by ANALMETR:36;
then b29 = b39 by A2, A5, A6, A10, A11, A20, A91, AFF_1:14, AFF_1:25;
then a19,b29 // a29,b39 by A92, AFF_1:2;
hence a1,b2 // a2,b3 by ANALMETR:36; :: thesis: verum
end;
hence a1,b2 // a2,b3 by A53; :: thesis: verum
end;
now :: thesis: ( b2 = b1 implies a1,b2 // a2,b3 )
A94: not LIN o9,b29,a39
proof
assume LIN o9,b29,a39 ; :: thesis: contradiction
then LIN o,b2,a3 by ANALMETR:40;
then LIN b2,o,a3 by A27;
then A95: b2,o // b2,a3 by ANALMETR:def 10;
LIN b2,o,b3 by A27, A36;
then b2,o // b2,b3 by ANALMETR:def 10;
then b2,a3 // b2,b3 by A2, A10, A95, ANALMETR:60;
hence contradiction by A39, ANALMETR:def 10; :: thesis: verum
end;
LIN a3,a1,o by A27, A34;
then A96: a3,a1 // a3,o by ANALMETR:def 10;
A97: a3 <> a1
proof
assume a3 = a1 ; :: thesis: contradiction
then LIN a39,a19,b29 by AFF_1:7;
hence contradiction by A39, ANALMETR:40; :: thesis: verum
end;
a3,a1 // a3,a2 by A35, ANALMETR:def 10;
then a3,o // a3,a2 by A96, A97, ANALMETR:60;
then LIN a3,o,a2 by ANALMETR:def 10;
then LIN o,a3,a2 by A27;
then A98: LIN o9,a39,a29 by ANALMETR:40;
assume A99: b2 = b1 ; :: thesis: a1,b2 // a2,b3
then b2,a3 // b2,a2 by A17, ANALMETR:59;
then b29,a39 // b29,a29 by ANALMETR:36;
then a39 = a29 by A98, A94, AFF_1:14;
hence a1,b2 // a2,b3 by A18, A99, ANALMETR:59; :: thesis: verum
end;
hence a1,b2 // a2,b3 by A41; :: thesis: verum
end;
now :: thesis: ( a1 = a3 implies a1,b2 // a2,b3 )
A100: not LIN o9,a19,b19
proof
o9,b19 // o9,b29 by A6, A7, A8, A19, AFF_1:39, AFF_1:41;
then A101: LIN o9,b19,b29 by AFF_1:def 1;
assume LIN o9,a19,b19 ; :: thesis: contradiction
then b19 in M9 by A2, A3, A13, A20, AFF_1:25;
hence contradiction by A2, A10, A15, A20, A101, AFF_1:25; :: thesis: verum
end;
o9,b19 // o9,b39 by A6, A7, A9, A19, AFF_1:39, AFF_1:41;
then A102: LIN o9,b19,b39 by AFF_1:def 1;
assume A103: a1 = a3 ; :: thesis: a1,b2 // a2,b3
then a1,b1 // a1,b3 by A18, ANALMETR:59;
then a19,b19 // a19,b39 by ANALMETR:36;
hence a1,b2 // a2,b3 by A17, A103, A100, A102, AFF_1:14; :: thesis: verum
end;
hence a1,b2 // a2,b3 by A21, A33; :: thesis: verum