let X be OrtAfPl; :: thesis: ( X is satisfying_MH1 implies X is satisfying_OSCH )
assume A1: X is satisfying_MH1 ; :: thesis: X is satisfying_OSCH
let a1 be Element of X; :: according to CONMETR:def 7 :: thesis: for a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X st M _|_ N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds
a3,a4 // b3,b4
let a2, a3, a4, b1, b2, b3, b4 be Element of X; :: thesis: for M, N being Subset of X st M _|_ N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds
a3,a4 // b3,b4
let M, N be Subset of X; :: thesis: ( M _|_ N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 implies a3,a4 // b3,b4 )
assume that
A2: M _|_ N and
A3: a1 in M and
A4: a3 in M and
A5: b1 in M and
A6: b3 in M and
A7: a2 in N and
A8: a4 in N and
A9: b2 in N and
A10: b4 in N and
A11: not a4 in M and
A12: not a2 in M and
A13: not b2 in M and
A14: not b4 in M and
A15: not a1 in N and
A16: not a3 in N and
A17: not b1 in N and
not b3 in N and
A18: a3,a2 // b3,b2 and
A19: a2,a1 // b2,b1 and
A20: a1,a4 // b1,b4 ; :: thesis: a3,a4 // b3,b4
reconsider M9 = M, N9 = N as Subset of AffinStruct(# the carrier of X, the CONGR of X #) ;
N is being_line by A2, ANALMETR:44;
then A21: N9 is being_line by ANALMETR:43;
reconsider b49 = b4, b19 = b1, b29 = b2, b39 = b3, a19 = a1, a29 = a2, a39 = a3, a49 = a4 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
M is being_line by A2, ANALMETR:44;
then A22: M9 is being_line by ANALMETR:43;
not M9 // N9
proof
assume M9 // N9 ; :: thesis: contradiction
then M // N by ANALMETR:46;
hence contradiction by A2, ANALMETR:52; :: thesis: verum
end;
then ex o9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) st
( o9 in M9 & o9 in N9 ) by A22, A21, AFF_1:58;
then consider o being Element of X such that
A23: o in M and
A24: o in N ;
reconsider o9 = o as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
A25: now :: thesis: ( b2 <> b4 implies a3,a4 // b3,b4 )
assume A26: b2 <> b4 ; :: thesis: a3,a4 // b3,b4
A27: now :: thesis: ( b1 <> b3 implies a3,a4 // b3,b4 )
consider e19 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A28: o9 <> e19 and
A29: e19 in M9 by A22, AFF_1:20;
reconsider e1 = e19 as Element of X ;
ex d49 being Element of AffinStruct(# the carrier of X, the CONGR of X #) st
( o9 <> d49 & d49 in N9 ) by A21, AFF_1:20;
then consider d4 being Element of X such that
A30: d4 in N and
A31: d4 <> o ;
reconsider d49 = d4 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
consider e2 being Element of X such that
A32: a1,a4 _|_ d4,e2 and
A33: e2 <> d4 by ANALMETR:39;
reconsider e29 = e2 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
assume A34: b1 <> b3 ; :: thesis: a3,a4 // b3,b4
not o9,e19 // d49,e29
proof
A35: a49 <> a29
proof
assume a49 = a29 ; :: thesis: contradiction
then a2,a1 // b1,b4 by A20, ANALMETR:59;
then b1,b4 // b2,b1 by A3, A12, A19, ANALMETR:60;
then b1,b4 // b1,b2 by ANALMETR:59;
then LIN b1,b4,b2 by ANALMETR:def 10;
then LIN b19,b49,b29 by ANALMETR:40;
then LIN b29,b49,b19 by AFF_1:6;
hence contradiction by A9, A10, A17, A21, A26, AFF_1:25; :: thesis: verum
end;
A36: a1 <> a3
proof
assume a1 = a3 ; :: thesis: contradiction
then a3,a2 // b2,b1 by A19, ANALMETR:59;
then b3,b2 // b2,b1 by A4, A12, A18, ANALMETR:60;
then b2,b3 // b2,b1 by ANALMETR:59;
then LIN b2,b3,b1 by ANALMETR:def 10;
then LIN b29,b39,b19 by ANALMETR:40;
then LIN b19,b39,b29 by AFF_1:6;
hence contradiction by A5, A6, A13, A22, A34, AFF_1:25; :: thesis: verum
end;
assume o9,e19 // d49,e29 ; :: thesis: contradiction
then o,e1 // d4,e2 by ANALMETR:36;
then A37: o,e1 _|_ a1,a4 by A32, A33, ANALMETR:62;
o9,e19 // a19,a39 by A3, A4, A22, A23, A29, AFF_1:39, AFF_1:41;
then o,e1 // a1,a3 by ANALMETR:36;
then A38: a1,a3 _|_ a1,a4 by A28, A37, ANALMETR:62;
a1,a3 _|_ a2,a4 by A2, A3, A4, A7, A8, ANALMETR:56;
then a1,a4 // a2,a4 by A38, A36, ANALMETR:63;
then a4,a2 // a4,a1 by ANALMETR:59;
then LIN a4,a2,a1 by ANALMETR:def 10;
then LIN a49,a29,a19 by ANALMETR:40;
hence contradiction by A7, A8, A15, A21, A35, AFF_1:25; :: thesis: verum
end;
then consider d19 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A39: LIN o9,e19,d19 and
A40: LIN d49,e29,d19 by AFF_1:60;
reconsider d1 = d19 as Element of X ;
consider e19 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A41: o9 <> e19 and
A42: e19 in N9 by A21, AFF_1:20;
A43: d1 in M by A22, A23, A28, A29, A39, AFF_1:25;
LIN d4,e2,d1 by A40, ANALMETR:40;
then d4,e2 // d4,d1 by ANALMETR:def 10;
then A44: d1,d4 // d4,e2 by ANALMETR:59;
then a1,a4 _|_ d1,d4 by A32, A33, ANALMETR:62;
then A45: b1,b4 _|_ d1,d4 by A3, A11, A20, ANALMETR:62;
reconsider e1 = e19 as Element of X ;
consider e2 being Element of X such that
A46: a2,a1 _|_ d1,e2 and
A47: e2 <> d1 by ANALMETR:39;
reconsider e29 = e2 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
not o9,e19 // e29,d19
proof
A48: a19 <> a39
proof
assume a19 = a39 ; :: thesis: contradiction
then a3,a2 // b2,b1 by A19, ANALMETR:59;
then b3,b2 // b2,b1 by A4, A12, A18, ANALMETR:60;
then b2,b3 // b2,b1 by ANALMETR:59;
then LIN b2,b3,b1 by ANALMETR:def 10;
then LIN b29,b39,b19 by ANALMETR:40;
then LIN b19,b39,b29 by AFF_1:6;
hence contradiction by A5, A6, A13, A22, A34, AFF_1:25; :: thesis: verum
end;
o9,e19 // a29,a49 by A7, A8, A21, A24, A42, AFF_1:39, AFF_1:41;
then A49: o,e1 // a2,a4 by ANALMETR:36;
A50: a2 <> a4
proof
assume a2 = a4 ; :: thesis: contradiction
then a2,a1 // b1,b4 by A20, ANALMETR:59;
then b1,b4 // b2,b1 by A3, A12, A19, ANALMETR:60;
then b1,b4 // b1,b2 by ANALMETR:59;
then LIN b1,b4,b2 by ANALMETR:def 10;
then LIN b19,b49,b29 by ANALMETR:40;
then LIN b29,b49,b19 by AFF_1:6;
hence contradiction by A9, A10, A17, A21, A26, AFF_1:25; :: thesis: verum
end;
assume o9,e19 // e29,d19 ; :: thesis: contradiction
then A51: o,e1 // e2,d1 by ANALMETR:36;
a2,a1 _|_ e2,d1 by A46, ANALMETR:61;
then o,e1 _|_ a2,a1 by A47, A51, ANALMETR:62;
then A52: a2,a1 _|_ a2,a4 by A41, A49, ANALMETR:62;
a3,a1 _|_ a2,a4 by A2, A3, A4, A7, A8, ANALMETR:56;
then a3,a1 // a2,a1 by A52, A50, ANALMETR:63;
then a1,a3 // a1,a2 by ANALMETR:59;
then LIN a1,a3,a2 by ANALMETR:def 10;
then LIN a19,a39,a29 by ANALMETR:40;
hence contradiction by A3, A4, A12, A22, A48, AFF_1:25; :: thesis: verum
end;
then consider d29 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A53: LIN o9,e19,d29 and
A54: LIN e29,d19,d29 by AFF_1:60;
reconsider d2 = d29 as Element of X ;
A55: d2 in N by A21, A24, A41, A42, A53, AFF_1:25;
LIN d19,d29,e29 by A54, AFF_1:6;
then LIN d1,d2,e2 by ANALMETR:40;
then d1,d2 // d1,e2 by ANALMETR:def 10;
then A56: d2,d1 // e2,d1 by ANALMETR:59;
A57: a2,a1 _|_ e2,d1 by A46, ANALMETR:61;
then A58: a2,a1 _|_ d2,d1 by A47, A56, ANALMETR:62;
consider e19 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A59: o9 <> e19 and
A60: e19 in M9 by A22, AFF_1:20;
reconsider e1 = e19 as Element of X ;
consider e2 being Element of X such that
A61: a3,a2 _|_ d2,e2 and
A62: e2 <> d2 by ANALMETR:39;
reconsider e29 = e2 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
not o9,e19 // e29,d29
proof
A63: a29 <> a49
proof
assume a29 = a49 ; :: thesis: contradiction
then a2,a1 // b1,b4 by A20, ANALMETR:59;
then b1,b4 // b2,b1 by A3, A12, A19, ANALMETR:60;
then b1,b4 // b1,b2 by ANALMETR:59;
then LIN b1,b4,b2 by ANALMETR:def 10;
then LIN b19,b49,b29 by ANALMETR:40;
then LIN b29,b49,b19 by AFF_1:6;
hence contradiction by A9, A10, A17, A21, A26, AFF_1:25; :: thesis: verum
end;
assume o9,e19 // e29,d29 ; :: thesis: contradiction
then o,e1 // e2,d2 by ANALMETR:36;
then o,e1 // d2,e2 by ANALMETR:59;
then A64: a3,a2 _|_ o,e1 by A61, A62, ANALMETR:62;
o,e1 _|_ a2,a4 by A2, A7, A8, A23, A60, ANALMETR:56;
then a3,a2 // a2,a4 by A59, A64, ANALMETR:63;
then a2,a4 // a2,a3 by ANALMETR:59;
then LIN a2,a4,a3 by ANALMETR:def 10;
then LIN a29,a49,a39 by ANALMETR:40;
hence contradiction by A7, A8, A16, A21, A63, AFF_1:25; :: thesis: verum
end;
then consider d39 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A65: LIN o9,e19,d39 and
A66: LIN e29,d29,d39 by AFF_1:60;
reconsider d3 = d39 as Element of X ;
A67: d3 in M by A22, A23, A59, A60, A65, AFF_1:25;
then A68: d3 <> d4 by A2, A22, A21, A23, A24, A30, A31, AFF_1:18;
a2,a1 _|_ d2,d1 by A47, A56, A57, ANALMETR:62;
then A69: b2,b1 _|_ d2,d1 by A3, A12, A19, ANALMETR:62;
LIN d29,d39,e29 by A66, AFF_1:6;
then LIN d2,d3,e2 by ANALMETR:40;
then d2,d3 // d2,e2 by ANALMETR:def 10;
then d3,d2 // d2,e2 by ANALMETR:59;
then A70: a3,a2 _|_ d3,d2 by A61, A62, ANALMETR:62;
then b3,b2 _|_ d3,d2 by A4, A12, A18, ANALMETR:62;
then A71: b3,b4 _|_ d3,d4 by A1, A2, A5, A6, A9, A10, A13, A14, A30, A43, A55, A67, A45, A69;
a1,a4 _|_ d1,d4 by A32, A33, A44, ANALMETR:62;
then a3,a4 _|_ d3,d4 by A1, A2, A3, A4, A7, A8, A11, A12, A30, A43, A55, A58, A70, A67;
hence a3,a4 // b3,b4 by A68, A71, ANALMETR:63; :: thesis: verum
end;
now :: thesis: ( b1 = b3 implies a3,a4 // b3,b4 )
A72: not LIN o9,a29,a19 by A7, A12, A15, A21, A23, A24, AFF_1:48, AFF_1:def 1;
A73: LIN o9,a19,a39 by A3, A4, A22, A23, AFF_1:21;
assume A74: b1 = b3 ; :: thesis: a3,a4 // b3,b4
then a2,a3 // b2,b1 by A18, ANALMETR:59;
then A75: a29,a39 // b29,b19 by ANALMETR:36;
a29,a19 // b29,b19 by A19, ANALMETR:36;
then a29,a19 // a29,a39 by A5, A13, A75, AFF_1:5;
hence a3,a4 // b3,b4 by A20, A74, A72, A73, AFF_1:14; :: thesis: verum
end;
hence a3,a4 // b3,b4 by A27; :: thesis: verum
end;
now :: thesis: ( b2 = b4 implies a3,a4 // b3,b4 )
A76: not LIN o9,a19,a49
proof
assume LIN o9,a19,a49 ; :: thesis: contradiction
then ex A9 being Subset of AffinStruct(# the carrier of X, the CONGR of X #) st
( A9 is being_line & o9 in A9 & a19 in A9 & a49 in A9 ) by AFF_1:21;
hence contradiction by A3, A11, A15, A22, A23, A24, AFF_1:18; :: thesis: verum
end;
assume A77: b2 = b4 ; :: thesis: a3,a4 // b3,b4
b1,b2 // a1,a2 by A19, ANALMETR:59;
then a1,a4 // a1,a2 by A5, A13, A20, A77, ANALMETR:60;
then A78: a19,a49 // a19,a29 by ANALMETR:36;
LIN o9,a49,a29 by A7, A8, A21, A24, AFF_1:21;
hence a3,a4 // b3,b4 by A18, A77, A78, A76, AFF_1:14; :: thesis: verum
end;
hence a3,a4 // b3,b4 by A25; :: thesis: verum