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