let X be OrtAfPl; :: thesis: ( X is satisfying_OSCH & X is satisfying_TDES implies X is satisfying_SCH )
assume that
A1: X is satisfying_OSCH and
A2: X is satisfying_TDES ; :: thesis: X is satisfying_SCH
let a1 be Element of X; :: according to CONMETR:def 6 :: thesis: for a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X st M is being_line & N is being_line & 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 is being_line & N is being_line & 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 is being_line & N is being_line & 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
A3: M is being_line and
A4: N is being_line and
A5: a1 in M and
A6: a3 in M and
A7: b1 in M and
A8: b3 in M and
A9: a2 in N and
A10: a4 in N and
A11: b2 in N and
A12: b4 in N and
A13: not a4 in M and
A14: not a2 in M and
A15: not b2 in M and
A16: not b4 in M and
A17: not a1 in N and
A18: not a3 in N and
A19: not b1 in N and
A20: not b3 in N and
A21: a3,a2 // b3,b2 and
A22: a2,a1 // b2,b1 and
A23: a1,a4 // b1,b4 ; :: thesis: a3,a4 // b3,b4
reconsider a19 = a1, a29 = a2, a39 = a3, a49 = a4, b19 = b1, b29 = b2, b39 = b3, b49 = b4 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 #) ;
A24: M9 is being_line by A3, ANALMETR:43;
A25: N9 is being_line by A4, ANALMETR:43;
A26: ( a1 <> b1 implies ( a2 <> b2 & a3 <> b3 & a4 <> b4 ) )
proof
assume A27: a1 <> b1 ; :: thesis: ( a2 <> b2 & a3 <> b3 & a4 <> b4 )
A28: now :: thesis: not a4 = b4
assume a4 = b4 ; :: thesis: contradiction
then a4,a1 // a4,b1 by A23, ANALMETR:59;
then LIN a4,a1,b1 by ANALMETR:def 10;
then LIN a49,a19,b19 by ANALMETR:40;
then LIN a19,b19,a49 by AFF_1:6;
hence contradiction by A5, A7, A13, A24, A27, AFF_1:25; :: thesis: verum
end;
A29: now :: thesis: not a2 = b2
assume a2 = b2 ; :: thesis: contradiction
then LIN a2,a1,b1 by A22, ANALMETR:def 10;
then LIN a29,a19,b19 by ANALMETR:40;
then LIN a19,b19,a29 by AFF_1:6;
hence contradiction by A5, A7, A14, A24, A27, AFF_1:25; :: thesis: verum
end;
A30: now :: thesis: not a3 = b3
assume a3 = b3 ; :: thesis: contradiction
then LIN a3,a2,b2 by A21, ANALMETR:def 10;
then LIN a39,a29,b29 by ANALMETR:40;
then LIN a29,b29,a39 by AFF_1:6;
hence contradiction by A9, A11, A18, A25, A29, AFF_1:25; :: thesis: verum
end;
assume ( a2 = b2 or a3 = b3 or a4 = b4 ) ; :: thesis: contradiction
hence contradiction by A29, A28, A30; :: thesis: verum
end;
A31: now :: thesis: ( a1 <> b1 implies a3,a4 // b3,b4 )
assume A32: a1 <> b1 ; :: thesis: a3,a4 // b3,b4
A33: now :: thesis: ( a2 = a4 implies a3,a4 // b3,b4 )
A34: not LIN a29,b19,b29
proof
assume LIN a29,b19,b29 ; :: thesis: contradiction
then LIN a29,b29,b19 by AFF_1:6;
hence contradiction by A9, A11, A19, A25, A26, A32, AFF_1:25; :: thesis: verum
end;
assume A35: a2 = a4 ; :: thesis: a3,a4 // b3,b4
then a2,a1 // b1,b4 by A23, ANALMETR:59;
then b2,b1 // b1,b4 by A5, A14, A22, ANALMETR:60;
then b1,b2 // b1,b4 by ANALMETR:59;
then A36: b19,b29 // b19,b49 by ANALMETR:36;
a29,b29 // a29,b49 by A9, A11, A12, A25, AFF_1:39, AFF_1:41;
then LIN a29,b29,b49 by AFF_1:def 1;
hence a3,a4 // b3,b4 by A21, A35, A34, A36, AFF_1:14; :: thesis: verum
end;
A37: now :: thesis: ( a2 <> a4 & a1 <> a3 implies a3,a4 // b3,b4 )
assume that
A38: a2 <> a4 and
A39: a1 <> a3 ; :: thesis: a3,a4 // b3,b4
A40: now :: thesis: ( M // N implies a3,a4 // b3,b4 )
consider e1 being Element of X such that
A41: b1,b2 // b1,e1 and
A42: b1 <> e1 by ANALMETR:39;
consider x being Element of X such that
A43: LIN a1,a2,x and
A44: a1 <> x and
A45: a2 <> x by Th2;
reconsider x9 = x as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
consider e2 being Element of X such that
A46: a1,b1 // x,e2 and
A47: x <> e2 by ANALMETR:39;
reconsider e19 = e1, e29 = e2 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
not b19,e19 // x9,e29 then consider y9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A48: LIN b19,e19,y9 and
A49: LIN x9,e29,y9 by AFF_1:60;
reconsider y = y9 as Element of X ;
A50: a1,a2 // a1,x by A43, ANALMETR:def 10;
A51: not LIN a2,b2,x
proof
A52: a2 <> b2
proof
assume a2 = b2 ; :: thesis: contradiction
then LIN a2,a1,b1 by A22, ANALMETR:def 10;
then LIN a29,a19,b19 by ANALMETR:40;
then LIN a19,b19,a29 by AFF_1:6;
hence contradiction by A5, A7, A14, A24, A32, AFF_1:25; :: thesis: verum
end;
LIN a19,a29,x9 by A43, ANALMETR:40;
then A53: LIN a29,x9,a19 by AFF_1:6;
assume LIN a2,b2,x ; :: thesis: contradiction
then LIN a29,b29,x9 by ANALMETR:40;
then x9 in N9 by A9, A11, A25, A52, AFF_1:25;
hence contradiction by A9, A17, A25, A45, A53, AFF_1:25; :: thesis: verum
end;
A54: not LIN a1,b1,a4
proof
assume LIN a1,b1,a4 ; :: thesis: contradiction
then LIN a19,b19,a49 by ANALMETR:40;
hence contradiction by A5, A7, A13, A24, A32, AFF_1:25; :: thesis: verum
end;
A55: not LIN a1,b1,x
proof
assume LIN a1,b1,x ; :: thesis: contradiction
then LIN a19,b19,x9 by ANALMETR:40;
then A56: x9 in M9 by A5, A7, A24, A32, AFF_1:25;
LIN a19,a29,x9 by A43, ANALMETR:40;
then LIN a19,x9,a29 by AFF_1:6;
hence contradiction by A5, A14, A24, A44, A56, AFF_1:25; :: thesis: verum
end;
assume A57: M // N ; :: thesis: a3,a4 // b3,b4
then M9 // N9 by ANALMETR:46;
then a39,b39 // a29,b29 by A6, A8, A9, A11, AFF_1:39;
then a3,b3 // a2,b2 by ANALMETR:36;
then A58: a2,b2 // a3,b3 by ANALMETR:59;
LIN x,e2,y by A49, ANALMETR:40;
then x,e2 // x,y by ANALMETR:def 10;
then A59: a1,b1 // x,y by A46, A47, ANALMETR:60;
A60: b1 <> y
proof
assume b1 = y ; :: thesis: contradiction
then b1,a1 // b1,x by A59, ANALMETR:59;
then LIN b1,a1,x by ANALMETR:def 10;
then LIN b19,a19,x9 by ANALMETR:40;
then A61: x9 in M9 by A5, A7, A24, A32, AFF_1:25;
LIN a19,a29,x9 by A43, ANALMETR:40;
then LIN a19,x9,a29 by AFF_1:6;
hence contradiction by A5, A14, A24, A44, A61, AFF_1:25; :: thesis: verum
end;
LIN b1,e1,y by A48, ANALMETR:40;
then b1,e1 // b1,y by ANALMETR:def 10;
then A62: b1,b2 // b1,y by A41, A42, ANALMETR:60;
then LIN b1,b2,y by ANALMETR:def 10;
then LIN b19,b29,y9 by ANALMETR:40;
then LIN y9,b19,b29 by AFF_1:6;
then LIN y,b1,b2 by ANALMETR:40;
then y,b1 // y,b2 by ANALMETR:def 10;
then A63: b1,y // b2,y by ANALMETR:59;
a1,a2 // b1,b2 by A22, ANALMETR:59;
then a1,a2 // b1,y by A7, A15, A62, ANALMETR:60;
then A64: a1,x // b1,y by A5, A14, A50, ANALMETR:60;
A65: not LIN x,y,a3
proof
A66: x <> y
proof
assume x = y ; :: thesis: contradiction
then x,a1 // x,b1 by A64, ANALMETR:59;
then LIN x,a1,b1 by ANALMETR:def 10;
then LIN x9,a19,b19 by ANALMETR:40;
then LIN a19,b19,x9 by AFF_1:6;
then A67: x9 in M9 by A5, A7, A24, A32, AFF_1:25;
LIN a19,a29,x9 by A43, ANALMETR:40;
then LIN x9,a19,a29 by AFF_1:6;
hence contradiction by A5, A14, A24, A44, A67, AFF_1:25; :: thesis: verum
end;
a19,a39 // a19,b19 by A5, A6, A7, A24, AFF_1:39, AFF_1:41;
then a1,a3 // a1,b1 by ANALMETR:36;
then A68: x,y // a1,a3 by A32, A59, ANALMETR:60;
assume LIN x,y,a3 ; :: thesis: contradiction
then x,y // x,a3 by ANALMETR:def 10;
then x,a3 // a1,a3 by A66, A68, ANALMETR:60;
then a3,a1 // a3,x by ANALMETR:59;
then LIN a3,a1,x by ANALMETR:def 10;
then LIN a39,a19,x9 by ANALMETR:40;
then A69: x9 in M9 by A5, A6, A24, A39, AFF_1:25;
LIN a19,a29,x9 by A43, ANALMETR:40;
then LIN a19,x9,a29 by AFF_1:6;
hence contradiction by A5, A14, A24, A44, A69, AFF_1:25; :: thesis: verum
end;
A70: not LIN x,y,a4
proof
A71: x <> y
proof
assume x = y ; :: thesis: contradiction
then x,a1 // x,b1 by A64, ANALMETR:59;
then LIN x,a1,b1 by ANALMETR:def 10;
then LIN x9,a19,b19 by ANALMETR:40;
then LIN a19,b19,x9 by AFF_1:6;
then A72: x9 in M9 by A5, A7, A24, A32, AFF_1:25;
LIN a19,a29,x9 by A43, ANALMETR:40;
then LIN x9,a19,a29 by AFF_1:6;
hence contradiction by A5, A14, A24, A44, A72, AFF_1:25; :: thesis: verum
end;
M9 // N9 by A57, ANALMETR:46;
then a19,b19 // a29,a49 by A5, A7, A9, A10, AFF_1:39;
then a1,b1 // a2,a4 by ANALMETR:36;
then A73: a2,a4 // x,y by A32, A59, ANALMETR:60;
assume LIN x,y,a4 ; :: thesis: contradiction
then x,y // x,a4 by ANALMETR:def 10;
then a2,a4 // x,a4 by A71, A73, ANALMETR:60;
then a4,a2 // a4,x by ANALMETR:59;
then LIN a4,a2,x by ANALMETR:def 10;
then LIN a49,a29,x9 by ANALMETR:40;
then A74: x9 in N9 by A9, A10, A25, A38, AFF_1:25;
LIN a19,a29,x9 by A43, ANALMETR:40;
then LIN a29,x9,a19 by AFF_1:6;
hence contradiction by A9, A17, A25, A45, A74, AFF_1:25; :: thesis: verum
end;
A75: not LIN a2,b2,a3
proof
A76: a2 <> b2
proof
assume a2 = b2 ; :: thesis: contradiction
then LIN a2,a1,b1 by A22, ANALMETR:def 10;
then LIN a29,a19,b19 by ANALMETR:40;
then LIN a19,b19,a29 by AFF_1:6;
hence contradiction by A5, A7, A14, A24, A32, AFF_1:25; :: thesis: verum
end;
assume LIN a2,b2,a3 ; :: thesis: contradiction
then LIN a29,b29,a39 by ANALMETR:40;
hence contradiction by A9, A11, A18, A25, A76, AFF_1:25; :: thesis: verum
end;
A77: ( X is satisfying_TDES implies X is satisfying_des ) LIN a19,a29,x9 by A43, ANALMETR:40;
then LIN x9,a19,a29 by AFF_1:6;
then LIN x,a1,a2 by ANALMETR:40;
then x,a1 // x,a2 by ANALMETR:def 10;
then a1,x // a2,x by ANALMETR:59;
then a2,x // b1,y by A44, A64, ANALMETR:60;
then A78: a2,x // b2,y by A60, A63, ANALMETR:60;
a19,b19 // a39,b39 by A5, A6, A7, A8, A24, AFF_1:39, AFF_1:41;
then a1,b1 // a3,b3 by ANALMETR:36;
then A79: x,y // a3,b3 by A32, A59, ANALMETR:60;
M9 // N9 by A57, ANALMETR:46;
then a19,b19 // a49,b49 by A5, A7, A10, A12, AFF_1:39;
then a1,b1 // a4,b4 by ANALMETR:36;
then A80: x,y // a4,b4 by A32, A59, ANALMETR:60;
M9 // N9 by A57, ANALMETR:46;
then a19,b19 // a29,b29 by A5, A7, A9, A11, AFF_1:39;
then a1,b1 // a2,b2 by ANALMETR:36;
then A81: a2,b2 // x,y by A32, A59, ANALMETR:60;
a2,a3 // b2,b3 by A21, ANALMETR:59;
then A82: x,a3 // y,b3 by A2, A77, A51, A75, A81, A58, A78;
M9 // N9 by A57, ANALMETR:46;
then a19,b19 // a49,b49 by A5, A7, A10, A12, AFF_1:39;
then a1,b1 // a4,b4 by ANALMETR:36;
then x,a4 // y,b4 by A2, A23, A59, A77, A55, A54, A64;
hence a3,a4 // b3,b4 by A2, A77, A82, A65, A70, A79, A80; :: thesis: verum
end;
now :: thesis: ( not M // N implies a3,a4 // b3,b4 )
assume not M // N ; :: thesis: a3,a4 // b3,b4
then not M9 // N9 by ANALMETR:46;
then consider o9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A83: o9 in M9 and
A84: o9 in N9 by A24, A25, AFF_1:58;
reconsider o = o9 as Element of X ;
consider K being Subset of X such that
A85: o in K and
A86: N _|_ K by A4, Th3;
reconsider K9 = K as Subset of AffinStruct(# the carrier of X, the CONGR of X #) ;
A87: K is being_line by A86, ANALMETR:44;
then A88: K9 is being_line by ANALMETR:43;
now :: thesis: ( K <> M implies a3,a4 // b3,b4 )
A89: ( not a2 in K & not a4 in K & not b2 in K & not b4 in K )
proof
A90: now :: thesis: for x being Element of X st x in N & o <> x holds
not x in K
let x be Element of X; :: thesis: ( x in N & o <> x implies not x in K )
assume that
A91: x in N and
A92: o <> x ; :: thesis: not x in K
assume x in K ; :: thesis: contradiction
then o,x _|_ o,x by A84, A85, A86, A91, ANALMETR:56;
hence contradiction by A92, ANALMETR:39; :: thesis: verum
end;
assume ( a2 in K or a4 in K or b2 in K or b4 in K ) ; :: thesis: contradiction
hence contradiction by A9, A10, A11, A12, A13, A14, A15, A16, A83, A90; :: thesis: verum
end;
A93: LIN o,a2,b2 by A4, A9, A11, A84, Th4;
A94: now :: thesis: not LIN a1,b1,a4
assume LIN a1,b1,a4 ; :: thesis: contradiction
then LIN a19,b19,a49 by ANALMETR:40;
hence contradiction by A5, A7, A13, A24, A32, AFF_1:25; :: thesis: verum
end;
A95: LIN o,a3,b3 by A3, A6, A8, A83, Th4;
A96: now :: thesis: not LIN a3,b3,a2
assume LIN a3,b3,a2 ; :: thesis: contradiction
then LIN a39,b39,a29 by ANALMETR:40;
hence contradiction by A6, A8, A14, A24, A26, A32, AFF_1:25; :: thesis: verum
end;
A97: LIN o,a1,b1 by A3, A5, A7, A83, Th4;
A98: now :: thesis: for x9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) ex y9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) st
( y9 in K9 & x9,y9 // N9 )
let x9 be Element of AffinStruct(# the carrier of X, the CONGR of X #); :: thesis: ex y9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) st
( y9 in K9 & x9,y9 // N9 )
consider D9 being Subset of AffinStruct(# the carrier of X, the CONGR of X #) such that
A99: x9 in D9 and
A100: N9 // D9 by A25, AFF_1:49;
reconsider D = D9 as Subset of the carrier of X ;
N // D by A100, ANALMETR:46;
then K _|_ D by A86, ANALMETR:52;
then consider y being Element of X such that
A101: y in K and
A102: y in D by ANALMETR:66;
reconsider y9 = y as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
take y9 = y9; :: thesis: ( y9 in K9 & x9,y9 // N9 )
thus ( y9 in K9 & x9,y9 // N9 ) by A99, A100, A101, A102, AFF_1:40; :: thesis: verum
end;
then consider d19 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A103: d19 in K9 and
A104: a19,d19 // N9 ;
consider e19 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A105: e19 in K9 and
A106: b19,e19 // N9 by A98;
consider d39 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A107: d39 in K9 and
A108: a39,d39 // N9 by A98;
consider e39 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A109: e39 in K9 and
A110: b39,e39 // N9 by A98;
reconsider d1 = d19, d3 = d39, e1 = e19, e3 = e39 as Element of X ;
A111: LIN o,d1,e1 by A85, A87, A103, A105, Th4;
A112: ( o <> e1 & o <> e3 & o <> d1 & o <> d3 )
proof
A113: now :: thesis: for x, y being Element of X
for x9, y9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) st x9,y9 // N9 & x = x9 & y = y9 & x in M & y in K & not x in N holds
not o = y
let x, y be Element of X; :: thesis: for x9, y9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) st x9,y9 // N9 & x = x9 & y = y9 & x in M & y in K & not x in N holds
not o = y
let x9, y9 be Element of AffinStruct(# the carrier of X, the CONGR of X #); :: thesis: ( x9,y9 // N9 & x = x9 & y = y9 & x in M & y in K & not x in N implies not o = y )
assume that
A114: x9,y9 // N9 and
A115: x = x9 and
A116: y = y9 and
x in M and
y in K and
A117: not x in N ; :: thesis: not o = y
assume o = y ; :: thesis: contradiction
then o9,x9 // N9 by A114, A116, AFF_1:34;
hence contradiction by A25, A84, A115, A117, AFF_1:23; :: thesis: verum
end;
assume ( not o <> e1 or not o <> e3 or not o <> d1 or not o <> d3 ) ; :: thesis: contradiction
hence contradiction by A5, A6, A7, A8, A17, A18, A19, A20, A103, A104, A107, A108, A109, A110, A105, A106, A113; :: thesis: verum
end;
a1,d1 // o,a2 by A9, A84, A104, Th6;
then A118: d1,a1 // o,a2 by ANALMETR:59;
A119: not e1 in N by A19, A106, AFF_1:35;
A120: not d3 in N by A18, A108, AFF_1:35;
a19,d19 // b19,e19 by A25, A104, A106, AFF_1:31;
then a1,d1 // b1,e1 by ANALMETR:36;
then A121: d1,a1 // e1,b1 by ANALMETR:59;
assume A122: K <> M ; :: thesis: a3,a4 // b3,b4
A123: now :: thesis: not LIN a3,b3,d3
assume LIN a3,b3,d3 ; :: thesis: contradiction
then LIN a39,b39,d39 by ANALMETR:40;
then d3 in M by A6, A8, A24, A26, A32, AFF_1:25;
hence contradiction by A3, A83, A85, A87, A122, A107, A112, Th5; :: thesis: verum
end;
A124: now :: thesis: not LIN a1,b1,d1
assume LIN a1,b1,d1 ; :: thesis: contradiction
then LIN a19,b19,d19 by ANALMETR:40;
then d1 in M by A5, A7, A24, A32, AFF_1:25;
hence contradiction by A3, A83, A85, A87, A122, A103, A112, Th5; :: thesis: verum
end;
a39,d39 // b39,e39 by A25, A108, A110, AFF_1:31;
then A125: a3,d3 // b3,e3 by ANALMETR:36;
then A126: d3,a3 // e3,b3 by ANALMETR:59;
A127: ( not LIN d3,e3,a3 & not LIN d3,e3,a4 )
proof
A128: d3 <> e3
proof
assume not d3 <> e3 ; :: thesis: contradiction
then LIN e3,a3,b3 by A126, ANALMETR:def 10;
then LIN e39,a39,b39 by ANALMETR:40;
then LIN a39,b39,e39 by AFF_1:6;
then e39 in M9 by A6, A8, A24, A26, A32, AFF_1:25;
hence contradiction by A24, A83, A85, A88, A122, A109, A112, AFF_1:18; :: thesis: verum
end;
assume ( LIN d3,e3,a3 or LIN d3,e3,a4 ) ; :: thesis: contradiction
then ( LIN d39,e39,a39 or LIN d39,e39,a49 ) by ANALMETR:40;
then ( a39 in K9 or a49 in K9 ) by A88, A107, A109, A128, AFF_1:25;
hence contradiction by A6, A10, A13, A18, A24, A25, A83, A84, A85, A86, A88, A122, AFF_1:18; :: thesis: verum
end;
A129: now :: thesis: not LIN a1,b1,a2
assume LIN a1,b1,a2 ; :: thesis: contradiction
then LIN a19,b19,a29 by ANALMETR:40;
hence contradiction by A5, A7, A14, A24, A32, AFF_1:25; :: thesis: verum
end;
A130: LIN o,a4,b4 by A4, A10, A12, A84, Th4;
a1,a2 // b1,b2 by A22, ANALMETR:59;
then d1,a2 // e1,b2 by A2, A14, A15, A17, A19, A83, A84, A112, A93, A97, A111, A124, A129, A121, A118;
then A131: a2,d1 // b2,e1 by ANALMETR:59;
A132: not e3 in N by A20, A110, AFF_1:35;
A133: LIN o,d3,e3 by A85, A87, A107, A109, Th4;
a1,d1 // o,a4 by A10, A84, A104, Th6;
then d1,a1 // o,a4 by ANALMETR:59;
then A134: d1,a4 // e1,b4 by A2, A13, A16, A17, A19, A23, A83, A84, A112, A97, A130, A111, A124, A94, A121;
A135: a3,d3 // o,a4 by A10, A84, A108, Th6;
A136: not d1 in N by A17, A104, AFF_1:35;
a3,d3 // o,a2 by A9, A84, A108, Th6;
then d3,a3 // o,a2 by ANALMETR:59;
then d3,a2 // e3,b2 by A2, A14, A15, A18, A20, A21, A83, A84, A112, A93, A95, A133, A123, A96, A126;
then d3,a4 // e3,b4 by A1, A9, A10, A11, A12, A86, A103, A107, A109, A105, A131, A134, A136, A120, A119, A132, A89;
hence a3,a4 // b3,b4 by A2, A13, A16, A18, A20, A83, A84, A112, A130, A95, A133, A125, A127, A135; :: thesis: verum
end;
hence a3,a4 // b3,b4 by A1, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A21, A22, A23, A86; :: thesis: verum
end;
hence a3,a4 // b3,b4 by A40; :: thesis: verum
end;
now :: thesis: ( a1 = a3 implies a3,a4 // b3,b4 )
A137: not LIN a19,b29,b19
proof
assume LIN a19,b29,b19 ; :: thesis: contradiction
then LIN a19,b19,b29 by AFF_1:6;
hence contradiction by A5, A7, A15, A24, A32, AFF_1:25; :: thesis: verum
end;
a19,b19 // a19,b39 by A5, A7, A8, A24, AFF_1:39, AFF_1:41;
then A138: LIN a19,b19,b39 by AFF_1:def 1;
assume A139: a1 = a3 ; :: thesis: a3,a4 // b3,b4
then a2,a1 // b2,b3 by A21, ANALMETR:59;
then b2,b1 // b2,b3 by A5, A14, A22, ANALMETR:60;
then b29,b19 // b29,b39 by ANALMETR:36;
hence a3,a4 // b3,b4 by A23, A139, A137, A138, AFF_1:14; :: thesis: verum
end;
hence a3,a4 // b3,b4 by A33, A37; :: thesis: verum
end;
A140: ( a1 = b1 implies ( a2 = b2 & a3 = b3 & a4 = b4 ) )
proof
assume A141: a1 = b1 ; :: thesis: ( a2 = b2 & a3 = b3 & a4 = b4 )
A142: now :: thesis: not a4 <> b4
LIN a1,a4,b4 by A23, A141, ANALMETR:def 10;
then LIN a19,a49,b49 by ANALMETR:40;
then A143: LIN a49,b49,a19 by AFF_1:6;
assume a4 <> b4 ; :: thesis: contradiction
hence contradiction by A10, A12, A17, A25, A143, AFF_1:25; :: thesis: verum
end;
A144: now :: thesis: not a2 <> b2
a1,a2 // a1,b2 by A22, A141, ANALMETR:59;
then LIN a1,a2,b2 by ANALMETR:def 10;
then LIN a19,a29,b29 by ANALMETR:40;
then A145: LIN a29,b29,a19 by AFF_1:6;
assume a2 <> b2 ; :: thesis: contradiction
hence contradiction by A9, A11, A17, A25, A145, AFF_1:25; :: thesis: verum
end;
A146: now :: thesis: not a3 <> b3
a2,a3 // a2,b3 by A21, A144, ANALMETR:59;
then LIN a2,a3,b3 by ANALMETR:def 10;
then LIN a29,a39,b39 by ANALMETR:40;
then A147: LIN a39,b39,a29 by AFF_1:6;
assume a3 <> b3 ; :: thesis: contradiction
hence contradiction by A6, A8, A14, A24, A147, AFF_1:25; :: thesis: verum
end;
assume ( a2 <> b2 or a3 <> b3 or a4 <> b4 ) ; :: thesis: contradiction
hence contradiction by A144, A142, A146; :: thesis: verum
end;
now :: thesis: ( a1 = b1 implies a3,a4 // b3,b4 )
assume a1 = b1 ; :: thesis: a3,a4 // b3,b4
then a39,a49 // b39,b49 by A140, AFF_1:2;
hence a3,a4 // b3,b4 by ANALMETR:36; :: thesis: verum
end;
hence a3,a4 // b3,b4 by A31; :: thesis: verum