let X be OrtAfPl; :: thesis: ( X is satisfying_MH1 & X is satisfying_MH2 implies X is satisfying_OPAP )
assume A1: X is satisfying_MH1 ; :: thesis: ( not X is satisfying_MH2 or X is satisfying_OPAP )
assume A2: X is satisfying_MH2 ; :: 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
A3: o in M and
A4: a1 in M and
A5: a2 in M and
A6: a3 in M and
A7: o in N and
A8: b1 in N and
A9: b2 in N and
A10: b3 in N and
A11: not b2 in M and
A12: not a3 in N and
A13: M _|_ N and
A14: o <> a1 and
A15: o <> a2 and
o <> a3 and
A16: o <> b1 and
o <> b2 and
A17: o <> b3 and
A18: a3,b2 // a2,b1 and
A19: 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;
N is being_line by A13, ANALMETR:62;
then A20: N' is being_line by ANALMETR:58;
M is being_line by A13, ANALMETR:62;
then A21: M' is being_line by ANALMETR:58;
A22: now
consider e1 being Element of X such that
A23: o,a3 // o,e1 and
A24: o <> e1 by ANALMETR:51;
consider d1 being Element of X such that
A25: o,b3 // o,d1 and
A26: o <> d1 by ANALMETR:51;
reconsider d1' = d1 as Element of (Af X) by ANALMETR:47;
consider e2 being Element of X such that
A27: a1,b3 _|_ d1,e2 and
A28: d1 <> e2 by ANALMETR:51;
reconsider e1' = e1, e2' = e2 as Element of (Af X) by ANALMETR:47;
assume that
A29: a1 <> a2 and
a2 <> a3 and
A30: a1 <> a3 ; :: thesis: ex d4 being Element of X st a1,b2 // a2,b3
A31: LIN o,b3,d1 by A25, ANALMETR:def 11;
then A32: LIN o',b3',d1' by ANALMETR:55;
N is being_line by A13, ANALMETR:62;
then A33: N' is being_line by ANALMETR:58;
then A34: o',b2' // o',b3' by A7, A9, A10, AFF_1:53, AFF_1:55;
then o,b2 // o,b3 by ANALMETR:48;
then A35: LIN o,b2,b3 by ANALMETR:def 11;
A36: b2 <> b3
proof
A37: not LIN o',b1',a2'
proof
o',a2' // o',a3' by A3, A5, A6, A21, AFF_1:53, AFF_1:55;
then A38: LIN o',a2',a3' by AFF_1:def 1;
assume LIN o',b1',a2' ; :: thesis: contradiction
then a2' in N' by A7, A8, A16, A20, AFF_1:39;
hence contradiction by A7, A12, A15, A20, A38, AFF_1:39; :: thesis: verum
end;
assume b2 = b3 ; :: thesis: contradiction
then a1,b1 // a2,b1 by A6, A11, A18, A19, ANALMETR:82;
then b1,a2 // b1,a1 by ANALMETR:81;
then A39: b1',a2' // b1',a1' by ANALMETR:48;
o',a2' // o',a1' by A3, A4, A5, A21, AFF_1:53, AFF_1:55;
then LIN o',a2',a1' by AFF_1:def 1;
hence contradiction by A29, A37, A39, AFF_1:23; :: thesis: verum
end;
A40: not LIN b2,a3,b3
proof
assume LIN b2,a3,b3 ; :: thesis: contradiction
then LIN b2',a3',b3' by ANALMETR:55;
then LIN b2',b3',a3' by AFF_1:15;
hence contradiction by A9, A10, A12, A36, A33, AFF_1:39; :: thesis: verum
end;
A41: a3 <> b3
proof
assume a3 = b3 ; :: thesis: contradiction
then LIN b2',a3',b3' by AFF_1:16;
hence contradiction by A40, ANALMETR:55; :: thesis: verum
end;
b2',b3' // b2',b1' by A8, A9, A10, A33, AFF_1:53, AFF_1:55;
then b2,b3 // b2,b1 by ANALMETR:48;
then A42: LIN b2,b3,b1 by ANALMETR:def 11;
M is being_line by A13, ANALMETR:62;
then A43: M' is being_line by ANALMETR:58;
then o',a3' // o',a1' by A3, A4, A6, AFF_1:53, AFF_1:55;
then A44: o,a3 // o,a1 by ANALMETR:48;
then A45: LIN o,a3,a1 by ANALMETR:def 11;
A46: not LIN a3,a1,b2
proof
assume LIN a3,a1,b2 ; :: thesis: contradiction
then LIN a3',a1',b2' by ANALMETR:55;
hence contradiction by A4, A6, A11, A30, A43, AFF_1:39; :: thesis: verum
end;
A47: a3 <> b2
proof
assume a3 = b2 ; :: thesis: contradiction
then LIN a3',a1',b2' by AFF_1:16;
hence contradiction by A46, ANALMETR:55; :: thesis: verum
end;
A48: o,a3 _|_ o,b3 by A3, A6, A7, A10, A13, ANALMETR:78;
not o,e1 // d1,e2
proof
reconsider e1' = e1, e2' = e2 as Element of (Af X) by ANALMETR:47;
assume o,e1 // d1,e2 ; :: thesis: contradiction
then o',e1' // d1',e2' by ANALMETR:48;
then d1',e2' // o',e1' by AFF_1:13;
then d1,e2 // o,e1 by ANALMETR:48;
then o,e1 _|_ a1,b3 by A27, A28, ANALMETR:84;
then o,a3 _|_ a1,b3 by A23, A24, ANALMETR:84;
then o,b3 // a1,b3 by A7, A12, A48, ANALMETR:85;
then o',b3' // a1',b3' by ANALMETR:48;
then b3',o' // b3',a1' by AFF_1:13;
then LIN b3',o',a1' by AFF_1:def 1;
then LIN o',b3',a1' by AFF_1:15;
then A49: o',b3' // o',a1' by AFF_1:def 1;
LIN o',b2',b3' by A35, ANALMETR:55;
then o',b2' // o',b3' by AFF_1:def 1;
then o',b3' // o',b2' by AFF_1:13;
then o',a1' // o',b2' by A17, A49, DIRAF:47;
then LIN o',a1',b2' by AFF_1:def 1;
then LIN a1',o',b2' by AFF_1:15;
then A50: a1',o' // a1',b2' by AFF_1:def 1;
LIN o',a3',a1' by A45, ANALMETR:55;
then LIN a1',o',a3' by AFF_1:15;
then a1',o' // a1',a3' by AFF_1:def 1;
then a1',b2' // a1',a3' by A14, A50, DIRAF:47;
then LIN a1',b2',a3' by AFF_1:def 1;
then LIN a3',a1',b2' by AFF_1:15;
hence contradiction by A46, ANALMETR:55; :: thesis: verum
end;
then not o',e1' // d1',e2' by ANALMETR:48;
then consider d2' being Element of (Af X) such that
A51: LIN o',e1',d2' and
A52: LIN d1',e2',d2' by AFF_1:74;
reconsider d2 = d2' as Element of X by ANALMETR:47;
LIN d1,e2,d2 by A52, ANALMETR:55;
then A53: d1,e2 // d1,d2 by ANALMETR:def 11;
then A54: a1,b3 _|_ d1,d2 by A27, A28, ANALMETR:84;
then A55: d1,d2 _|_ b3,a1 by ANALMETR:83;
LIN o,e1,d2 by A51, ANALMETR:55;
then o,e1 // o,d2 by ANALMETR:def 11;
then A56: o,a3 // o,d2 by A23, A24, ANALMETR:82;
then A57: LIN o,a3,d2 by ANALMETR:def 11;
then A58: LIN o',a3',d2' by ANALMETR:55;
consider e1 being Element of X such that
A59: o,b3 // o,e1 and
A60: o <> e1 by ANALMETR:51;
consider e2 being Element of X such that
A61: b3,a3 _|_ d2,e2 and
A62: d2 <> e2 by ANALMETR:51;
reconsider e1' = e1, e2' = e2 as Element of (Af X) by ANALMETR:47;
not o,e1 // d2,e2
proof
reconsider e1' = e1, e2' = e2 as Element of (Af X) by ANALMETR:47;
assume o,e1 // d2,e2 ; :: thesis: contradiction
then o',e1' // d2',e2' by ANALMETR:48;
then d2',e2' // o',e1' by AFF_1:13;
then d2,e2 // o,e1 by ANALMETR:48;
then o,e1 _|_ b3,a3 by A61, A62, ANALMETR:84;
then o,b3 _|_ b3,a3 by A59, A60, ANALMETR:84;
then b3,a3 // o,a3 by A17, A48, ANALMETR:85;
then b3',a3' // o',a3' by ANALMETR:48;
then a3',b3' // a3',o' by AFF_1:13;
then LIN a3',b3',o' by AFF_1:def 1;
then LIN b3',o',a3' by AFF_1:15;
then A63: b3',o' // b3',a3' by AFF_1:def 1;
LIN o',b2',b3' by A35, ANALMETR:55;
then LIN b3',o',b2' by AFF_1:15;
then b3',o' // b3',b2' by AFF_1:def 1;
then b3',a3' // b3',b2' by A17, A63, DIRAF:47;
then LIN b3',a3',b2' by AFF_1:def 1;
then LIN b2',a3',b3' by AFF_1:15;
hence contradiction by A40, ANALMETR:55; :: thesis: verum
end;
then not o',e1' // d2',e2' by ANALMETR:48;
then consider d3' being Element of (Af X) such that
A64: LIN o',e1',d3' and
A65: LIN d2',e2',d3' by AFF_1:74;
reconsider d3 = d3' as Element of X by ANALMETR:47;
LIN d2,e2,d3 by A65, ANALMETR:55;
then A66: d2,e2 // d2,d3 by ANALMETR:def 11;
then A67: b3,a3 _|_ d2,d3 by A61, A62, ANALMETR:84;
then d2,d3 _|_ a3,b3 by ANALMETR:83;
then A68: d2,d3 _|_ a1,b1 by A19, A41, ANALMETR:84;
LIN o,e1,d3 by A64, ANALMETR:55;
then o,e1 // o,d3 by ANALMETR:def 11;
then A69: o,b3 // o,d3 by A59, A60, ANALMETR:82;
then A70: LIN o,b3,d3 by ANALMETR:def 11;
then A71: LIN o',b3',d3' by ANALMETR:55;
consider e2 being Element of X such that
A72: a3,b2 _|_ d3,e2 and
A73: d3 <> e2 by ANALMETR:51;
consider e1 being Element of X such that
A74: o,a3 // o,e1 and
A75: o <> e1 by ANALMETR:51;
reconsider e1' = e1, e2' = e2 as Element of (Af X) by ANALMETR:47;
not o,e1 // d3,e2
proof
reconsider e1' = e1, e2' = e2 as Element of (Af X) by ANALMETR:47;
LIN o',b2',b3' by A35, ANALMETR:55;
then LIN b2',o',b3' by AFF_1:15;
then A76: b2',o' // b2',b3' by AFF_1:def 1;
assume o,e1 // d3,e2 ; :: thesis: contradiction
then o',e1' // d3',e2' by ANALMETR:48;
then d3',e2' // o',e1' by AFF_1:13;
then d3,e2 // o,e1 by ANALMETR:48;
then o,e1 _|_ a3,b2 by A72, A73, ANALMETR:84;
then o,a3 _|_ a3,b2 by A74, A75, ANALMETR:84;
then A77: o,b3 // a3,b2 by A7, A12, A48, ANALMETR:85;
LIN o',b2',b3' by A35, ANALMETR:55;
then LIN o',b3',b2' by AFF_1:15;
then LIN o,b3,b2 by ANALMETR:55;
then o,b3 // o,b2 by ANALMETR:def 11;
then o,b2 // a3,b2 by A17, A77, ANALMETR:82;
then o',b2' // a3',b2' by ANALMETR:48;
then b2',o' // b2',a3' by AFF_1:13;
then b2',a3' // b2',b3' by A3, A11, A76, DIRAF:47;
then LIN b2',a3',b3' by AFF_1:def 1;
hence contradiction by A40, ANALMETR:55; :: thesis: verum
end;
then not o',e1' // d3',e2' by ANALMETR:48;
then consider d4' being Element of (Af X) such that
A78: LIN o',e1',d4' and
A79: LIN d3',e2',d4' by AFF_1:74;
reconsider d4 = d4' as Element of X by ANALMETR:47;
LIN d3,e2,d4 by A79, ANALMETR:55;
then A80: d3,e2 // d3,d4 by ANALMETR:def 11;
then A81: d3,d4 _|_ a3,b2 by A72, A73, ANALMETR:84;
LIN o,e1,d4 by A78, ANALMETR:55;
then o,e1 // o,d4 by ANALMETR:def 11;
then A82: o,a3 // o,d4 by A74, A75, ANALMETR:82;
then A83: LIN o,a3,d4 by ANALMETR:def 11;
then A84: LIN o',a3',d4' by ANALMETR:55;
A85: a3,b2 _|_ d3,d4 by A72, A73, A80, ANALMETR:84;
then ( d3,d4 _|_ a2,b1 or a3 = b2 ) by A18, ANALMETR:84;
then A86: d3,d4 _|_ b1,a2 by A47, ANALMETR:83;
A87: d2 <> o
proof
o,a3 _|_ o,d1 by A17, A48, A25, ANALMETR:84;
then A88: d1,o _|_ o,a3 by ANALMETR:83;
assume d2 = o ; :: thesis: contradiction
then d1,o _|_ a1,b3 by A27, A28, A53, ANALMETR:84;
then o,a3 // a1,b3 by A26, A88, ANALMETR:85;
then a1,b3 // o,a1 by A7, A12, A44, ANALMETR:82;
then a1',b3' // o',a1' by ANALMETR:48;
then a1',b3' // a1',o' by AFF_1:13;
then LIN a1',b3',o' by AFF_1:def 1;
then LIN o',b3',a1' by AFF_1:15;
then A89: o',b3' // o',a1' by AFF_1:def 1;
LIN o',b2',b3' by A35, ANALMETR:55;
then LIN o',b3',b2' by AFF_1:15;
then o',b3' // o',b2' by AFF_1:def 1;
then o',a1' // o',b2' by A17, A89, DIRAF:47;
then LIN o',a1',b2' by AFF_1:def 1;
then LIN a1',o',b2' by AFF_1:15;
then A90: a1',o' // a1',b2' by AFF_1:def 1;
LIN o',a3',a1' by A45, ANALMETR:55;
then LIN a1',o',a3' by AFF_1:15;
then a1',o' // a1',a3' by AFF_1:def 1;
then a1',b2' // a1',a3' by A14, A90, DIRAF:47;
then LIN a1',b2',a3' by AFF_1:def 1;
then LIN a3',a1',b2' by AFF_1:15;
hence contradiction by A46, ANALMETR:55; :: thesis: verum
end;
A91: not LIN d1,d2,d3
proof
A92: d2 <> d3
proof
assume d2 = d3 ; :: thesis: contradiction
then o',b3' // o',d2' by A69, ANALMETR:48;
then o',d2' // o',b3' by AFF_1:13;
then o,d2 // o,b3 by ANALMETR:48;
then o,b3 // o,a3 by A56, A87, ANALMETR:82;
then o',b3' // o',a3' by ANALMETR:48;
then LIN o',b3',a3' by AFF_1:def 1;
then LIN b3',o',a3' by AFF_1:15;
then b3',o' // b3',a3' by AFF_1:def 1;
then A93: b3,o // b3,a3 by ANALMETR:48;
LIN o',b2',b3' by A35, ANALMETR:55;
then LIN b3',o',b2' by AFF_1:15;
then b3',o' // b3',b2' by AFF_1:def 1;
then b3,o // b3,b2 by ANALMETR:48;
then b3,b2 // b3,a3 by A17, A93, ANALMETR:82;
then LIN b3,b2,a3 by ANALMETR:def 11;
then LIN b3',b2',a3' by ANALMETR:55;
then LIN b2',a3',b3' by AFF_1:15;
hence contradiction by A40, ANALMETR:55; :: thesis: verum
end;
A94: d1 <> d2
proof
assume d1 = d2 ; :: thesis: contradiction
then o',a3' // o',d1' by A56, ANALMETR:48;
then o',d1' // o',a3' by AFF_1:13;
then o,d1 // o,a3 by ANALMETR:48;
then o,b3 // o,a3 by A25, A26, ANALMETR:82;
then o',b3' // o',a3' by ANALMETR:48;
then LIN o',b3',a3' by AFF_1:def 1;
then LIN b3',o',a3' by AFF_1:15;
then b3',o' // b3',a3' by AFF_1:def 1;
then A95: b3,o // b3,a3 by ANALMETR:48;
LIN o',b2',b3' by A35, ANALMETR:55;
then LIN b3',o',b2' by AFF_1:15;
then b3',o' // b3',b2' by AFF_1:def 1;
then b3,o // b3,b2 by ANALMETR:48;
then b3,b2 // b3,a3 by A17, A95, ANALMETR:82;
then LIN b3,b2,a3 by ANALMETR:def 11;
then LIN b3',b2',a3' by ANALMETR:55;
then LIN b2',a3',b3' by AFF_1:15;
hence contradiction by A40, ANALMETR:55; :: thesis: verum
end;
assume LIN d1,d2,d3 ; :: thesis: contradiction
then LIN d1',d2',d3' by ANALMETR:55;
then LIN d2',d1',d3' by AFF_1:15;
then d2',d1' // d2',d3' by AFF_1:def 1;
then d1',d2' // d2',d3' by AFF_1:13;
then d1,d2 // d2,d3 by ANALMETR:48;
then d2,d3 _|_ a1,b3 by A54, A94, ANALMETR:84;
then a1,b3 // b3,a3 by A67, A92, ANALMETR:85;
then a1',b3' // b3',a3' by ANALMETR:48;
then b3',a1' // b3',a3' by AFF_1:13;
then LIN b3',a1',a3' by AFF_1:def 1;
then LIN a1',a3',b3' by AFF_1:15;
then a1',a3' // a1',b3' by AFF_1:def 1;
then A96: a1,a3 // a1,b3 by ANALMETR:48;
A97: a1 <> a3
proof
assume a1 = a3 ; :: thesis: contradiction
then LIN a3',a1',b2' by AFF_1:16;
hence contradiction by A46, ANALMETR:55; :: thesis: verum
end;
LIN o',a3',a1' by A45, ANALMETR:55;
then LIN a1',a3',o' by AFF_1:15;
then a1',a3' // a1',o' by AFF_1:def 1;
then a1,a3 // a1,o by ANALMETR:48;
then a1,o // a1,b3 by A97, A96, ANALMETR:82;
then LIN a1,o,b3 by ANALMETR:def 11;
then LIN a1',o',b3' by ANALMETR:55;
then LIN o',b3',a1' by AFF_1:15;
then A98: o',b3' // o',a1' by AFF_1:def 1;
o',b3' // o',b2' by A34, AFF_1:13;
then o',a1' // o',b2' by A17, A98, DIRAF:47;
then LIN o',a1',b2' by AFF_1:def 1;
then LIN a1',o',b2' by AFF_1:15;
then a1',o' // a1',b2' by AFF_1:def 1;
then A99: a1,o // a1,b2 by ANALMETR:48;
LIN o',a3',a1' by A45, ANALMETR:55;
then LIN a1',o',a3' by AFF_1:15;
then a1',o' // a1',a3' by AFF_1:def 1;
then a1,o // a1,a3 by ANALMETR:48;
then a1,b2 // a1,a3 by A14, A99, ANALMETR:82;
then LIN a1,b2,a3 by ANALMETR:def 11;
then LIN a1',b2',a3' by ANALMETR:55;
then LIN a3',a1',b2' by AFF_1:15;
hence contradiction by A46, ANALMETR:55; :: thesis: verum
end;
A100: d2 <> d4
proof
A101: d2 <> d3
proof
assume d2 = d3 ; :: thesis: contradiction
then LIN d1',d2',d3' by AFF_1:16;
hence contradiction by A91, ANALMETR:55; :: thesis: verum
end;
assume d2 = d4 ; :: thesis: contradiction
then a3,b2 _|_ d2,d3 by A85, ANALMETR:83;
then a3,b2 // b3,a3 by A67, A101, ANALMETR:85;
then a3,b2 // a3,b3 by ANALMETR:81;
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 A9, A10, A12, A20, A36, AFF_1:39; :: thesis: verum
end;
LIN o',b3',b3' by AFF_1:16;
then A102: LIN d1',d3',b3' by A17, A32, A71, AFF_1:17;
then consider A' being Subset of (Af X) such that
A103: A' is being_line and
A104: d1' in A' and
A105: d3' in A' and
A106: b3' in A' by AFF_1:33;
reconsider A = A' as Subset of X by ANALMETR:57;
A107: d1' <> d3'
proof
assume d1' = d3' ; :: thesis: contradiction
then LIN d1',d2',d3' by AFF_1:16;
hence contradiction by A91, ANALMETR:55; :: thesis: verum
end;
then A' = Line d1',d3' by A103, A104, A105, AFF_1:38;
then A108: A = Line d1,d3 by ANALMETR:56;
LIN o',b2',b3' by A35, ANALMETR:55;
then A109: LIN o',b3',b2' by AFF_1:15;
then A110: b2 in A by A17, A32, A71, A103, A104, A105, A107, AFF_1:17, AFF_1:39;
A111: o <> d3
proof
assume d3 = o ; :: thesis: contradiction
then A112: d2,o _|_ b3,a3 by A61, A62, A66, ANALMETR:84;
o,b3 _|_ o,d2 by A7, A12, A48, A56, ANALMETR:84;
then d2,o _|_ o,b3 by ANALMETR:83;
then o,b3 // b3,a3 by A87, A112, ANALMETR:85;
then o',b3' // b3',a3' by ANALMETR:48;
then A113: b3',o' // b3',a3' by AFF_1:13;
LIN o',b2',b3' by A35, ANALMETR:55;
then LIN b3',o',b2' by AFF_1:15;
then b3',o' // b3',b2' by AFF_1:def 1;
then b3',a3' // b3',b2' by A17, A113, DIRAF:47;
then LIN b3',a3',b2' by AFF_1:def 1;
then LIN b2',a3',b3' by AFF_1:15;
hence contradiction by A40, ANALMETR:55; :: thesis: verum
end;
A114: o <> d4
proof
o,a3 _|_ o,d3 by A17, A48, A69, ANALMETR:84;
then A115: d3,o _|_ o,a3 by ANALMETR:83;
assume d4 = o ; :: thesis: contradiction
then d3,o _|_ a3,b2 by A72, A73, A80, ANALMETR:84;
then o,a3 // a3,b2 by A111, A115, ANALMETR:85;
then o',a3' // a3',b2' by ANALMETR:48;
then A116: a3',o' // a3',b2' by AFF_1:13;
LIN o',a3',a1' by A45, ANALMETR:55;
then LIN a3',o',a1' by AFF_1:15;
then a3',o' // a3',a1' by AFF_1:def 1;
then a3',b2' // a3',a1' by A7, A12, A116, DIRAF:47;
then LIN a3',b2',a1' by AFF_1:def 1;
then LIN a3',a1',b2' by AFF_1:15;
hence contradiction by A46, ANALMETR:55; :: thesis: verum
end;
A117: not LIN d1,d4,d3
proof
A118: d1 <> d3
proof
A119: d1 <> d2 assume d1 = d3 ; :: thesis: contradiction
then a3,b3 _|_ d1,d2 by A67, ANALMETR:83;
then a1,b3 // a3,b3 by A54, A119, ANALMETR:85;
then a1',b3' // a3',b3' by ANALMETR:48;
then b3',a1' // b3',a3' by AFF_1:13;
then LIN b3',a1',a3' by AFF_1:def 1;
then LIN a1',a3',b3' by AFF_1:15;
then a1',a3' // a1',b3' by AFF_1:def 1;
then A121: a1,a3 // a1,b3 by ANALMETR:48;
A122: a1 <> a3
proof
assume a1 = a3 ; :: thesis: contradiction
then LIN a3',a1',b2' by AFF_1:16;
hence contradiction by A46, ANALMETR:55; :: thesis: verum
end;
LIN o',a3',a1' by A45, ANALMETR:55;
then LIN a1',a3',o' by AFF_1:15;
then a1',a3' // a1',o' by AFF_1:def 1;
then a1,a3 // a1,o by ANALMETR:48;
then a1,o // a1,b3 by A122, A121, ANALMETR:82;
then LIN a1,o,b3 by ANALMETR:def 11;
then LIN a1',o',b3' by ANALMETR:55;
then LIN o',b3',a1' by AFF_1:15;
then A123: o',b3' // o',a1' by AFF_1:def 1;
o',b3' // o',b2' by A34, AFF_1:13;
then o',a1' // o',b2' by A17, A123, DIRAF:47;
then LIN o',a1',b2' by AFF_1:def 1;
then LIN a1',o',b2' by AFF_1:15;
then a1',o' // a1',b2' by AFF_1:def 1;
then A124: a1,o // a1,b2 by ANALMETR:48;
LIN o',a3',a1' by A45, ANALMETR:55;
then LIN a1',o',a3' by AFF_1:15;
then a1',o' // a1',a3' by AFF_1:def 1;
then a1,o // a1,a3 by ANALMETR:48;
then a1,b2 // a1,a3 by A14, A124, ANALMETR:82;
then LIN a1,b2,a3 by ANALMETR:def 11;
then LIN a1',b2',a3' by ANALMETR:55;
then LIN a3',a1',b2' by AFF_1:15;
hence contradiction by A46, ANALMETR:55; :: thesis: verum
end;
assume LIN d1,d4,d3 ; :: thesis: contradiction
then LIN d1',d4',d3' by ANALMETR:55;
then A125: LIN d1',d3',d4' by AFF_1:15;
A126: b2' <> b3'
proof
assume b2' = b3' ; :: thesis: contradiction
then LIN b2',a3',b3' by AFF_1:16;
hence contradiction by A40, ANALMETR:55; :: thesis: verum
end;
LIN o',b2',b3' by A35, ANALMETR:55;
then LIN b2',b3',o' by AFF_1:15;
then A127: b2',b3' // b2',o' by AFF_1:def 1;
LIN d1',d3',b2' by A17, A32, A71, A109, AFF_1:17;
then LIN b2',b3',d4' by A102, A118, A125, AFF_1:17;
then b2',b3' // b2',d4' by AFF_1:def 1;
then b2',o' // b2',d4' by A127, A126, DIRAF:47;
then LIN b2',o',d4' by AFF_1:def 1;
then LIN o',d4',b2' by AFF_1:15;
then A128: o',d4' // o',b2' by AFF_1:def 1;
o',a3' // o',d4' by A82, ANALMETR:48;
then o',d4' // o',a3' by AFF_1:13;
then o',b2' // o',a3' by A114, A128, DIRAF:47;
then LIN o',b2',a3' by AFF_1:def 1;
then LIN b2',o',a3' by AFF_1:15;
then A129: b2',o' // b2',a3' by AFF_1:def 1;
LIN o',b2',b3' by A35, ANALMETR:55;
then LIN b2',o',b3' by AFF_1:15;
then b2',o' // b2',b3' by AFF_1:def 1;
then b2',a3' // b2',b3' by A3, A11, A129, DIRAF:47;
then LIN b2',a3',b3' by AFF_1:def 1;
hence contradiction by A40, ANALMETR:55; :: thesis: verum
end;
A130: not d4 in A
proof
assume d4 in A ; :: thesis: contradiction
then d1',d4' // d1',d3' by A103, A104, A105, AFF_1:53, AFF_1:55;
then LIN d1',d4',d3' by AFF_1:def 1;
hence contradiction by A117, ANALMETR:55; :: thesis: verum
end;
A131: d2,d3 _|_ b3,a3 by A61, A62, A66, ANALMETR:84;
take d4 = d4; :: thesis: a1,b2 // a2,b3
LIN o',b3',d1' by A31, ANALMETR:55;
then A132: o',b3' // o',d1' by AFF_1:def 1;
LIN o',a3',a1' by A45, ANALMETR:55;
then A133: LIN d2',d4',a1' by A7, A12, A58, A84, AFF_1:17;
then consider K' being Subset of (Af X) such that
A134: K' is being_line and
A135: d2' in K' and
A136: d4' in K' and
A137: a1' in K' by AFF_1:33;
reconsider K = K' as Subset of X by ANALMETR:57;
LIN o',a3',a3' by AFF_1:16;
then A138: a3 in K by A7, A12, A58, A84, A100, A134, A135, A136, AFF_1:17, AFF_1:39;
a3',a1' // a3',a2' by A4, A5, A6, A43, AFF_1:53, AFF_1:55;
then a3,a1 // a3,a2 by ANALMETR:48;
then A139: LIN a3,a1,a2 by ANALMETR:def 11;
A140: ( LIN d1,d3,b3 & LIN d1,d3,b1 & LIN d2,d4,a1 & LIN d2,d4,a2 )
proof
A141: b3' <> b2'
proof
assume b3' = b2' ; :: thesis: contradiction
then LIN b2',a3',b3' by AFF_1:16;
hence contradiction by A40, ANALMETR:55; :: thesis: verum
end;
LIN o',b2',b3' by A35, ANALMETR:55;
then LIN b3',b2',o' by AFF_1:15;
then A142: b3',b2' // b3',o' by AFF_1:def 1;
LIN b2',b3',b1' by A42, ANALMETR:55;
then LIN b3',b2',b1' by AFF_1:15;
then b3',b2' // b3',b1' by AFF_1:def 1;
then b3',b1' // b3',o' by A142, A141, DIRAF:47;
then LIN b3',b1',o' by AFF_1:def 1;
then A143: LIN o',b3',b1' by AFF_1:15;
A144: LIN o',b3',d3' by A70, ANALMETR:55;
LIN o',b3',d1' by A31, ANALMETR:55;
then A145: LIN d1',d3',b1' by A17, A143, A144, AFF_1:17;
reconsider o' = o, a1' = a1, a2' = a2, a3' = a3, d2' = d2, d4' = d4 as Element of (Af X) by ANALMETR:47;
A146: a3' <> a1'
proof
assume a1' = a3' ; :: thesis: contradiction
then LIN a3',a1',b2' by AFF_1:16;
hence contradiction by A46, ANALMETR:55; :: thesis: verum
end;
LIN o',a3',a1' by A45, ANALMETR:55;
then LIN a3',a1',o' by AFF_1:15;
then A147: a3',a1' // a3',o' by AFF_1:def 1;
LIN a3',a1',a2' by A139, ANALMETR:55;
then a3',a1' // a3',a2' by AFF_1:def 1;
then a3',a2' // a3',o' by A147, A146, DIRAF:47;
then LIN a3',a2',o' by AFF_1:def 1;
then A148: LIN o',a3',a2' by AFF_1:15;
A149: LIN o',a3',d4' by A83, ANALMETR:55;
LIN o',a3',d2' by A57, ANALMETR:55;
then LIN d2',d4',a2' by A7, A12, A148, A149, AFF_1:17;
hence ( LIN d1,d3,b3 & LIN d1,d3,b1 & LIN d2,d4,a1 & LIN d2,d4,a2 ) by A102, A133, A145, ANALMETR:55; :: thesis: verum
end;
LIN o',b3',d3' by A70, ANALMETR:55;
then o',b3' // o',d3' by AFF_1:def 1;
then o',d1' // o',d3' by A17, A132, DIRAF:47;
then LIN o',d1',d3' by AFF_1:def 1;
then LIN d1',o',d3' by AFF_1:15;
then d1',o' // d1',d3' by AFF_1:def 1;
then o',d1' // d1',d3' by AFF_1:13;
then A150: o,d1 // d1,d3 by ANALMETR:48;
o,b3 // o,d1 by A132, ANALMETR:48;
then o,d1 _|_ o,a3 by A17, A48, ANALMETR:84;
then A151: o,a3 _|_ d1,d3 by A26, A150, ANALMETR:84;
LIN o',a3',d2' by A57, ANALMETR:55;
then A152: o',a3' // o',d2' by AFF_1:def 1;
then o,a3 // o,d2 by ANALMETR:48;
then A153: o,d2 _|_ d1,d3 by A7, A12, A151, ANALMETR:84;
A154: not d2 in A
proof
assume d2 in A ; :: thesis: contradiction
then d1',d2' // d1',d3' by A103, A104, A105, AFF_1:53, AFF_1:55;
then LIN d1',d2',d3' by AFF_1:def 1;
hence contradiction by A91, ANALMETR:55; :: thesis: verum
end;
LIN o',a3',d4' by A83, ANALMETR:55;
then o',a3' // o',d4' by AFF_1:def 1;
then o',d2' // o',d4' by A7, A12, A152, DIRAF:47;
then LIN o',d2',d4' by AFF_1:def 1;
then LIN d2',o',d4' by AFF_1:15;
then d2',o' // d2',d4' by AFF_1:def 1;
then o',d2' // d2',d4' by AFF_1:13;
then o,d2 // d2,d4 by ANALMETR:48;
then A155: d1,d3 _|_ d2,d4 by A87, A153, ANALMETR:84;
K' = Line d2',d4' by A100, A134, A135, A136, AFF_1:38;
then K = Line d2,d4 by ANALMETR:56;
then A156: A _|_ K by A155, A100, A107, A108, ANALMETR:63;
reconsider d1' = d1, d2' = d2, d3' = d3, d4' = d4, b3' = b3, a1' = a1, b1' = b1, a2' = a2 as Element of (Af X) by ANALMETR:47;
LIN d1',d3',b3' by A140, ANALMETR:55;
then consider A' being Subset of (Af X) such that
A157: A' is being_line and
A158: d1' in A' and
A159: d3' in A' and
A160: b3' in A' by AFF_1:33;
A161: d1' <> d3'
proof
assume d1' = d3' ; :: thesis: contradiction
then LIN d1',d2',d3' by AFF_1:16;
hence contradiction by A91, ANALMETR:55; :: thesis: verum
end;
reconsider A = A' as Subset of X by ANALMETR:57;
LIN d1',d3',b1' by A140, ANALMETR:55;
then A162: b1 in A by A157, A158, A159, A161, AFF_1:39;
A163: not d2 in A
proof
assume d2 in A ; :: thesis: contradiction
then d1',d2' // d1',d3' by A157, A158, A159, AFF_1:53, AFF_1:55;
then d1,d2 // d1,d3 by ANALMETR:48;
hence contradiction by A91, ANALMETR:def 11; :: thesis: verum
end;
A164: d1 <> d4
proof
LIN o',a3',d4' by A83, ANALMETR:55;
then A165: LIN o',d4',a3' by AFF_1:15;
LIN o',d4',o' by AFF_1:16;
then A166: o',d4' // o',a3' by A165, AFF_1:19;
A167: LIN o',b3',o' by AFF_1:16;
LIN o',b2',b3' by A35, ANALMETR:55;
then A168: LIN o',b3',b2' by AFF_1:15;
LIN o',b3',d1' by A31, ANALMETR:55;
then LIN o',d1',b2' by A17, A167, A168, AFF_1:17;
then A169: o',d1' // o',b2' by AFF_1:def 1;
assume d1 = d4 ; :: thesis: contradiction
then o',a3' // o',b2' by A114, A169, A166, DIRAF:47;
then LIN o',a3',b2' by AFF_1:def 1;
then LIN a3',b2',o' by AFF_1:15;
then a3',b2' // a3',o' by AFF_1:def 1;
then A170: a3',o' // a3',b2' by AFF_1:13;
LIN o',a3',a1' by A45, ANALMETR:55;
then LIN a3',o',a1' by AFF_1:15;
then a3',o' // a3',a1' by AFF_1:def 1;
then a3',b2' // a3',a1' by A7, A12, A170, DIRAF:47;
then LIN a3',b2',a1' by AFF_1:def 1;
then LIN a3',a1',b2' by AFF_1:15;
hence contradiction by A46, ANALMETR:55; :: thesis: verum
end;
A171: not d4 in A
proof
assume d4 in A ; :: thesis: contradiction
then d1',d4' // d1',d3' by A157, A158, A159, AFF_1:53, AFF_1:55;
then d1,d4 // d1,d3 by ANALMETR:48;
hence contradiction by A117, ANALMETR:def 11; :: thesis: verum
end;
LIN d2',d4',a1' by A140, ANALMETR:55;
then consider K' being Subset of (Af X) such that
A172: K' is being_line and
A173: d2' in K' and
A174: d4' in K' and
A175: a1' in K' by AFF_1:33;
reconsider K = K' as Subset of X by ANALMETR:57;
LIN d2',d4',a2' by A140, ANALMETR:55;
then A176: a2 in K by A100, A172, A173, A174, AFF_1:39;
K' = Line d2',d4' by A100, A172, A173, A174, AFF_1:38;
then A177: K = Line d2,d4 by ANALMETR:56;
A' = Line d1',d3' by A157, A158, A159, A161, AFF_1:38;
then A = Line d1,d3 by ANALMETR:56;
then A _|_ K by A155, A100, A161, A177, ANALMETR:63;
then A178: d1,d4 _|_ b3,a2 by A1, A68, A86, A55, A158, A159, A160, A173, A174, A175, A163, A171, A162, A176, Def3;
d1,d2 _|_ a1,b3 by A27, A28, A53, ANALMETR:84;
then d1,d4 _|_ a1,b2 by A2, A131, A81, A104, A105, A106, A135, A136, A137, A154, A130, A156, A110, A138, Def4;
then ( a1,b2 // b3,a2 or d1 = d4 ) by A178, ANALMETR:85;
then a1',b2' // b3',a2' by A164, ANALMETR:48;
then a1',b2' // a2',b3' by AFF_1:13;
hence a1,b2 // a2,b3 by ANALMETR:48; :: thesis: verum
end;
now
A179: now
o',b2' // o',b3' by A7, A9, A10, A20, AFF_1:53, AFF_1:55;
then A180: LIN o',b2',b3' by AFF_1:def 1;
assume A181: a1 = a2 ; :: thesis: a1,b2 // a2,b3
a1 <> b1
proof
o',a1' // o',a3' by A3, A4, A6, A21, AFF_1:53, AFF_1:55;
then A182: LIN o',a1',a3' by AFF_1:def 1;
assume a1 = b1 ; :: thesis: contradiction
hence contradiction by A7, A8, A12, A14, A20, A182, AFF_1:39; :: thesis: verum
end;
then a3,b2 // a3,b3 by A18, A19, A181, ANALMETR:82;
then a3',b2' // a3',b3' by ANALMETR:48;
then b2' = b3' by A3, A6, A7, A11, A12, A21, A180, AFF_1:23, AFF_1:39;
then a1',b2' // a2',b3' by A181, AFF_1:11;
hence a1,b2 // a2,b3 by ANALMETR:48; :: thesis: verum
end;
A183: now
A184: 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 A7, A8, A12, A16, A20, AFF_1:39; :: thesis: verum
end;
o',b1' // o',b3' by A7, A8, A10, A20, AFF_1:53, AFF_1:55;
then A185: LIN o',b1',b3' by AFF_1:def 1;
assume A186: a1 = a3 ; :: thesis: a1,b2 // a2,b3
then a3,b1 // a3,b3 by A19, ANALMETR:81;
then a3',b1' // a3',b3' by ANALMETR:48;
hence a1,b2 // a2,b3 by A18, A186, A184, A185, AFF_1:23; :: thesis: verum
end;
A187: now
A188: 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 A7, A8, A12, A16, A20, AFF_1:39; :: thesis: verum
end;
o',b1' // o',b2' by A7, A8, A9, A20, AFF_1:53, AFF_1:55;
then A189: LIN o',b1',b2' by AFF_1:def 1;
assume A190: a2 = a3 ; :: thesis: a1,b2 // a2,b3
then a3,b1 // a3,b2 by A18, ANALMETR:81;
then a3',b1' // a3',b2' by ANALMETR:48;
then a2,b3 // a1,b2 by A19, A190, A188, A189, AFF_1:23;
hence a1,b2 // a2,b3 by ANALMETR:81; :: thesis: verum
end;
assume ( a1 = a2 or a2 = a3 or a1 = a3 ) ; :: thesis: a1,b2 // a2,b3
hence a1,b2 // a2,b3 by A179, A187, A183; :: thesis: verum
end;
hence a1,b2 // a2,b3 by A22; :: thesis: verum