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 ; :: according to CONMETR:def 6 :: thesis: for a2, a3, a4, b1, b2, b3, b4 being Element of
for M, N being Subset of 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 ; :: thesis: for M, N being Subset of 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 ; :: 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 a1' = a1, a2' = a2, a3' = a3, a4' = a4, b1' = b1, b2' = b2, b3' = b3, b4' = b4 as Element of by ANALMETR:47;
reconsider M' = M, N' = N as Subset of by ANALMETR:57;
A24: M' is being_line by A3, ANALMETR:58;
A25: N' is being_line by A4, ANALMETR:58;
A26: ( a1 <> b1 implies ( a2 <> b2 & a3 <> b3 & a4 <> b4 ) )
proof
assume A27: a1 <> b1 ; :: thesis: ( a2 <> b2 & a3 <> b3 & a4 <> b4 )
A28: now
assume a4 = b4 ; :: thesis: contradiction
then a4,a1 // a4,b1 by A23, ANALMETR:81;
then LIN a4,a1,b1 by ANALMETR:def 11;
then LIN a4',a1',b1' by ANALMETR:55;
then LIN a1',b1',a4' by AFF_1:15;
hence contradiction by A5, A7, A13, A24, A27, AFF_1:39; :: thesis: verum
end;
A29: now
assume a2 = b2 ; :: thesis: contradiction
then LIN a2,a1,b1 by A22, ANALMETR:def 11;
then LIN a2',a1',b1' by ANALMETR:55;
then LIN a1',b1',a2' by AFF_1:15;
hence contradiction by A5, A7, A14, A24, A27, AFF_1:39; :: thesis: verum
end;
A30: now
assume a3 = b3 ; :: thesis: contradiction
then LIN a3,a2,b2 by A21, ANALMETR:def 11;
then LIN a3',a2',b2' by ANALMETR:55;
then LIN a2',b2',a3' by AFF_1:15;
hence contradiction by A9, A11, A18, A25, A29, AFF_1:39; :: 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
assume A32: a1 <> b1 ; :: thesis: a3,a4 // b3,b4
A33: now
A34: not LIN a2',b1',b2'
proof
assume LIN a2',b1',b2' ; :: thesis: contradiction
then LIN a2',b2',b1' by AFF_1:15;
hence contradiction by A9, A11, A19, A25, A26, A32, AFF_1:39; :: thesis: verum
end;
assume A35: a2 = a4 ; :: thesis: a3,a4 // b3,b4
then a2,a1 // b1,b4 by A23, ANALMETR:81;
then b2,b1 // b1,b4 by A5, A14, A22, ANALMETR:82;
then b1,b2 // b1,b4 by ANALMETR:81;
then A36: b1',b2' // b1',b4' by ANALMETR:48;
a2',b2' // a2',b4' by A9, A11, A12, A25, AFF_1:53, AFF_1:55;
then LIN a2',b2',b4' by AFF_1:def 1;
hence a3,a4 // b3,b4 by A21, A35, A34, A36, AFF_1:23; :: thesis: verum
end;
A37: now
assume that
A38: a2 <> a4 and
A39: a1 <> a3 ; :: thesis: a3,a4 // b3,b4
A40: now
consider e1 being Element of such that
A41: b1,b2 // b1,e1 and
A42: b1 <> e1 by ANALMETR:51;
consider x being Element of such that
A43: LIN a1,a2,x and
A44: a1 <> x and
A45: a2 <> x by A5, A14, Th2;
reconsider x' = x as Element of by ANALMETR:47;
consider e2 being Element of such that
A46: a1,b1 // x,e2 and
A47: x <> e2 by ANALMETR:51;
reconsider e1' = e1, e2' = e2 as Element of by ANALMETR:47;
not b1',e1' // x',e2' then consider y' being Element of such that
A48: LIN b1',e1',y' and
A49: LIN x',e2',y' by AFF_1:74;
reconsider y = y' as Element of by ANALMETR:47;
A50: a1,a2 // a1,x by A43, ANALMETR:def 11;
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 11;
then LIN a2',a1',b1' by ANALMETR:55;
then LIN a1',b1',a2' by AFF_1:15;
hence contradiction by A5, A7, A14, A24, A32, AFF_1:39; :: thesis: verum
end;
LIN a1',a2',x' by A43, ANALMETR:55;
then A53: LIN a2',x',a1' by AFF_1:15;
assume LIN a2,b2,x ; :: thesis: contradiction
then LIN a2',b2',x' by ANALMETR:55;
then x' in N' by A9, A11, A25, A52, AFF_1:39;
hence contradiction by A9, A17, A25, A45, A53, AFF_1:39; :: thesis: verum
end;
A54: not LIN a1,b1,a4
proof
assume LIN a1,b1,a4 ; :: thesis: contradiction
then LIN a1',b1',a4' by ANALMETR:55;
hence contradiction by A5, A7, A13, A24, A32, AFF_1:39; :: thesis: verum
end;
A55: not LIN a1,b1,x
proof
assume LIN a1,b1,x ; :: thesis: contradiction
then LIN a1',b1',x' by ANALMETR:55;
then A56: x' in M' by A5, A7, A24, A32, AFF_1:39;
LIN a1',a2',x' by A43, ANALMETR:55;
then LIN a1',x',a2' by AFF_1:15;
hence contradiction by A5, A14, A24, A44, A56, AFF_1:39; :: thesis: verum
end;
assume A57: M // N ; :: thesis: a3,a4 // b3,b4
then M' // N' by ANALMETR:64;
then a3',b3' // a2',b2' by A6, A8, A9, A11, AFF_1:53;
then a3,b3 // a2,b2 by ANALMETR:48;
then A58: a2,b2 // a3,b3 by ANALMETR:81;
LIN x,e2,y by A49, ANALMETR:55;
then x,e2 // x,y by ANALMETR:def 11;
then A59: a1,b1 // x,y by A46, A47, ANALMETR:82;
A60: b1 <> y
proof
assume b1 = y ; :: thesis: contradiction
then b1,a1 // b1,x by A59, ANALMETR:81;
then LIN b1,a1,x by ANALMETR:def 11;
then LIN b1',a1',x' by ANALMETR:55;
then A61: x' in M' by A5, A7, A24, A32, AFF_1:39;
LIN a1',a2',x' by A43, ANALMETR:55;
then LIN a1',x',a2' by AFF_1:15;
hence contradiction by A5, A14, A24, A44, A61, AFF_1:39; :: thesis: verum
end;
LIN b1,e1,y by A48, ANALMETR:55;
then b1,e1 // b1,y by ANALMETR:def 11;
then A62: b1,b2 // b1,y by A41, A42, ANALMETR:82;
then LIN b1,b2,y by ANALMETR:def 11;
then LIN b1',b2',y' by ANALMETR:55;
then LIN y',b1',b2' by AFF_1:15;
then LIN y,b1,b2 by ANALMETR:55;
then y,b1 // y,b2 by ANALMETR:def 11;
then A63: b1,y // b2,y by ANALMETR:81;
a1,a2 // b1,b2 by A22, ANALMETR:81;
then a1,a2 // b1,y by A7, A15, A62, ANALMETR:82;
then A64: a1,x // b1,y by A5, A14, A50, ANALMETR:82;
A65: not LIN x,y,a3
proof
A66: x <> y
proof
assume x = y ; :: thesis: contradiction
then x,a1 // x,b1 by A64, ANALMETR:81;
then LIN x,a1,b1 by ANALMETR:def 11;
then LIN x',a1',b1' by ANALMETR:55;
then LIN a1',b1',x' by AFF_1:15;
then A67: x' in M' by A5, A7, A24, A32, AFF_1:39;
LIN a1',a2',x' by A43, ANALMETR:55;
then LIN x',a1',a2' by AFF_1:15;
hence contradiction by A5, A14, A24, A44, A67, AFF_1:39; :: thesis: verum
end;
a1',a3' // a1',b1' by A5, A6, A7, A24, AFF_1:53, AFF_1:55;
then a1,a3 // a1,b1 by ANALMETR:48;
then A68: x,y // a1,a3 by A32, A59, ANALMETR:82;
assume LIN x,y,a3 ; :: thesis: contradiction
then x,y // x,a3 by ANALMETR:def 11;
then x,a3 // a1,a3 by A66, A68, ANALMETR:82;
then a3,a1 // a3,x by ANALMETR:81;
then LIN a3,a1,x by ANALMETR:def 11;
then LIN a3',a1',x' by ANALMETR:55;
then A69: x' in M' by A5, A6, A24, A39, AFF_1:39;
LIN a1',a2',x' by A43, ANALMETR:55;
then LIN a1',x',a2' by AFF_1:15;
hence contradiction by A5, A14, A24, A44, A69, AFF_1:39; :: 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:81;
then LIN x,a1,b1 by ANALMETR:def 11;
then LIN x',a1',b1' by ANALMETR:55;
then LIN a1',b1',x' by AFF_1:15;
then A72: x' in M' by A5, A7, A24, A32, AFF_1:39;
LIN a1',a2',x' by A43, ANALMETR:55;
then LIN x',a1',a2' by AFF_1:15;
hence contradiction by A5, A14, A24, A44, A72, AFF_1:39; :: thesis: verum
end;
M' // N' by A57, ANALMETR:64;
then a1',b1' // a2',a4' by A5, A7, A9, A10, AFF_1:53;
then a1,b1 // a2,a4 by ANALMETR:48;
then A73: a2,a4 // x,y by A32, A59, ANALMETR:82;
assume LIN x,y,a4 ; :: thesis: contradiction
then x,y // x,a4 by ANALMETR:def 11;
then a2,a4 // x,a4 by A71, A73, ANALMETR:82;
then a4,a2 // a4,x by ANALMETR:81;
then LIN a4,a2,x by ANALMETR:def 11;
then LIN a4',a2',x' by ANALMETR:55;
then A74: x' in N' by A9, A10, A25, A38, AFF_1:39;
LIN a1',a2',x' by A43, ANALMETR:55;
then LIN a2',x',a1' by AFF_1:15;
hence contradiction by A9, A17, A25, A45, A74, AFF_1:39; :: 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 11;
then LIN a2',a1',b1' by ANALMETR:55;
then LIN a1',b1',a2' by AFF_1:15;
hence contradiction by A5, A7, A14, A24, A32, AFF_1:39; :: thesis: verum
end;
assume LIN a2,b2,a3 ; :: thesis: contradiction
then LIN a2',b2',a3' by ANALMETR:55;
hence contradiction by A9, A11, A18, A25, A76, AFF_1:39; :: thesis: verum
end;
A77: ( X is satisfying_TDES implies X is satisfying_des ) LIN a1',a2',x' by A43, ANALMETR:55;
then LIN x',a1',a2' by AFF_1:15;
then LIN x,a1,a2 by ANALMETR:55;
then x,a1 // x,a2 by ANALMETR:def 11;
then a1,x // a2,x by ANALMETR:81;
then a2,x // b1,y by A44, A64, ANALMETR:82;
then A78: a2,x // b2,y by A60, A63, ANALMETR:82;
a1',b1' // a3',b3' by A5, A6, A7, A8, A24, AFF_1:53, AFF_1:55;
then a1,b1 // a3,b3 by ANALMETR:48;
then A79: x,y // a3,b3 by A32, A59, ANALMETR:82;
M' // N' by A57, ANALMETR:64;
then a1',b1' // a4',b4' by A5, A7, A10, A12, AFF_1:53;
then a1,b1 // a4,b4 by ANALMETR:48;
then A80: x,y // a4,b4 by A32, A59, ANALMETR:82;
M' // N' by A57, ANALMETR:64;
then a1',b1' // a2',b2' by A5, A7, A9, A11, AFF_1:53;
then a1,b1 // a2,b2 by ANALMETR:48;
then A81: a2,b2 // x,y by A32, A59, ANALMETR:82;
a2,a3 // b2,b3 by A21, ANALMETR:81;
then A82: x,a3 // y,b3 by A2, A77, A51, A75, A81, A58, A78, Def8;
M' // N' by A57, ANALMETR:64;
then a1',b1' // a4',b4' by A5, A7, A10, A12, AFF_1:53;
then a1,b1 // a4,b4 by ANALMETR:48;
then x,a4 // y,b4 by A2, A23, A59, A77, A55, A54, A64, Def8;
hence a3,a4 // b3,b4 by A2, A77, A82, A65, A70, A79, A80, Def8; :: thesis: verum
end;
now
assume not M // N ; :: thesis: a3,a4 // b3,b4
then not M' // N' by ANALMETR:64;
then consider o' being Element of such that
A83: o' in M' and
A84: o' in N' by A24, A25, AFF_1:72;
reconsider o = o' as Element of by ANALMETR:47;
consider K being Subset of such that
A85: o in K and
A86: N _|_ K by A4, Th3;
reconsider K' = K as Subset of by ANALMETR:57;
A87: K is being_line by A86, ANALMETR:62;
then A88: K' is being_line by ANALMETR:58;
now
A89: ( not a2 in K & not a4 in K & not b2 in K & not b4 in K )
proof
A90: now
let x be Element of ; :: 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:78;
hence contradiction by A92, ANALMETR:51; :: 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
assume LIN a1,b1,a4 ; :: thesis: contradiction
then LIN a1',b1',a4' by ANALMETR:55;
hence contradiction by A5, A7, A13, A24, A32, AFF_1:39; :: thesis: verum
end;
A95: LIN o,a3,b3 by A3, A6, A8, A83, Th4;
A96: now
assume LIN a3,b3,a2 ; :: thesis: contradiction
then LIN a3',b3',a2' by ANALMETR:55;
hence contradiction by A6, A8, A14, A24, A26, A32, AFF_1:39; :: thesis: verum
end;
A97: LIN o,a1,b1 by A3, A5, A7, A83, Th4;
A98: now
let x' be Element of ; :: thesis: ex y' being Element of st
( y' in K' & x',y' // N' )
consider D' being Subset of such that
A99: x' in D' and
A100: N' // D' by A25, AFF_1:63;
reconsider D = D' as Subset of by ANALMETR:57;
N // D by A100, ANALMETR:64;
then K _|_ D by A86, ANALMETR:73;
then consider y being Element of such that
A101: y in K and
A102: y in D by ANALMETR:88;
reconsider y' = y as Element of by ANALMETR:47;
take y' = y'; :: thesis: ( y' in K' & x',y' // N' )
thus ( y' in K' & x',y' // N' ) by A99, A100, A101, A102, AFF_1:54; :: thesis: verum
end;
then consider d1' being Element of such that
A103: d1' in K' and
A104: a1',d1' // N' ;
consider e1' being Element of such that
A105: e1' in K' and
A106: b1',e1' // N' by A98;
consider d3' being Element of such that
A107: d3' in K' and
A108: a3',d3' // N' by A98;
consider e3' being Element of such that
A109: e3' in K' and
A110: b3',e3' // N' by A98;
reconsider d1 = d1', d3 = d3', e1 = e1', e3 = e3' as Element of by ANALMETR:47;
A111: LIN o,d1,e1 by A85, A87, A103, A105, Th4;
A112: ( o <> e1 & o <> e3 & o <> d1 & o <> d3 )
proof
A113: now
let x, y be Element of ; :: thesis: for x', y' being Element of st x',y' // N' & x = x' & y = y' & x in M & y in K & not x in N holds
not o = y
let x', y' be Element of ; :: thesis: ( x',y' // N' & x = x' & y = y' & x in M & y in K & not x in N implies not o = y )
assume that
A114: x',y' // N' and
A115: x = x' and
A116: y = y' and
x in M and
y in K and
A117: not x in N ; :: thesis: not o = y
assume o = y ; :: thesis: contradiction
then o',x' // N' by A114, A116, AFF_1:48;
hence contradiction by A25, A84, A115, A117, AFF_1:37; :: 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:81;
A119: not e1 in N by A19, A106, AFF_1:49;
A120: not d3 in N by A18, A108, AFF_1:49;
a1',d1' // b1',e1' by A25, A104, A106, AFF_1:45;
then a1,d1 // b1,e1 by ANALMETR:48;
then A121: d1,a1 // e1,b1 by ANALMETR:81;
assume A122: K <> M ; :: thesis: a3,a4 // b3,b4
A123: now
assume LIN a3,b3,d3 ; :: thesis: contradiction
then LIN a3',b3',d3' by ANALMETR:55;
then d3 in M by A6, A8, A24, A26, A32, AFF_1:39;
hence contradiction by A3, A83, A85, A87, A122, A107, A112, Th5; :: thesis: verum
end;
A124: now
assume LIN a1,b1,d1 ; :: thesis: contradiction
then LIN a1',b1',d1' by ANALMETR:55;
then d1 in M by A5, A7, A24, A32, AFF_1:39;
hence contradiction by A3, A83, A85, A87, A122, A103, A112, Th5; :: thesis: verum
end;
a3',d3' // b3',e3' by A25, A108, A110, AFF_1:45;
then A125: a3,d3 // b3,e3 by ANALMETR:48;
then A126: d3,a3 // e3,b3 by ANALMETR:81;
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 11;
then LIN e3',a3',b3' by ANALMETR:55;
then LIN a3',b3',e3' by AFF_1:15;
then e3' in M' by A6, A8, A24, A26, A32, AFF_1:39;
hence contradiction by A24, A83, A85, A88, A122, A109, A112, AFF_1:30; :: thesis: verum
end;
assume ( LIN d3,e3,a3 or LIN d3,e3,a4 ) ; :: thesis: contradiction
then ( LIN d3',e3',a3' or LIN d3',e3',a4' ) by ANALMETR:55;
then ( a3' in K' or a4' in K' ) by A88, A107, A109, A128, AFF_1:39;
hence contradiction by A6, A10, A13, A18, A24, A25, A83, A84, A85, A86, A88, A122, AFF_1:30; :: thesis: verum
end;
A129: now
assume LIN a1,b1,a2 ; :: thesis: contradiction
then LIN a1',b1',a2' by ANALMETR:55;
hence contradiction by A5, A7, A14, A24, A32, AFF_1:39; :: thesis: verum
end;
A130: LIN o,a4,b4 by A4, A10, A12, A84, Th4;
a1,a2 // b1,b2 by A22, ANALMETR:81;
then d1,a2 // e1,b2 by A2, A14, A15, A17, A19, A83, A84, A112, A93, A97, A111, A124, A129, A121, A118, Def5;
then A131: a2,d1 // b2,e1 by ANALMETR:81;
A132: not e3 in N by A20, A110, AFF_1:49;
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:81;
then A134: d1,a4 // e1,b4 by A2, A13, A16, A17, A19, A23, A83, A84, A112, A97, A130, A111, A124, A94, A121, Def5;
A135: a3,d3 // o,a4 by A10, A84, A108, Th6;
A136: not d1 in N by A17, A104, AFF_1:49;
a3,d3 // o,a2 by A9, A84, A108, Th6;
then d3,a3 // o,a2 by ANALMETR:81;
then d3,a2 // e3,b2 by A2, A14, A15, A18, A20, A21, A83, A84, A112, A93, A95, A133, A123, A96, A126, Def5;
then d3,a4 // e3,b4 by A1, A9, A10, A11, A12, A86, A103, A107, A109, A105, A131, A134, A136, A120, A119, A132, A89, Def7;
hence a3,a4 // b3,b4 by A2, A13, A16, A18, A20, A83, A84, A112, A130, A95, A133, A125, A127, A135, Def5; :: 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, Def7; :: thesis: verum
end;
hence a3,a4 // b3,b4 by A40; :: thesis: verum
end;
now
A137: not LIN a1',b2',b1'
proof
assume LIN a1',b2',b1' ; :: thesis: contradiction
then LIN a1',b1',b2' by AFF_1:15;
hence contradiction by A5, A7, A15, A24, A32, AFF_1:39; :: thesis: verum
end;
a1',b1' // a1',b3' by A5, A7, A8, A24, AFF_1:53, AFF_1:55;
then A138: LIN a1',b1',b3' by AFF_1:def 1;
assume A139: a1 = a3 ; :: thesis: a3,a4 // b3,b4
then a2,a1 // b2,b3 by A21, ANALMETR:81;
then b2,b1 // b2,b3 by A5, A14, A22, ANALMETR:82;
then b2',b1' // b2',b3' by ANALMETR:48;
hence a3,a4 // b3,b4 by A23, A139, A137, A138, AFF_1:23; :: 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
LIN a1,a4,b4 by A23, A141, ANALMETR:def 11;
then LIN a1',a4',b4' by ANALMETR:55;
then A143: LIN a4',b4',a1' by AFF_1:15;
assume a4 <> b4 ; :: thesis: contradiction
hence contradiction by A10, A12, A17, A25, A143, AFF_1:39; :: thesis: verum
end;
A144: now
a1,a2 // a1,b2 by A22, A141, ANALMETR:81;
then LIN a1,a2,b2 by ANALMETR:def 11;
then LIN a1',a2',b2' by ANALMETR:55;
then A145: LIN a2',b2',a1' by AFF_1:15;
assume a2 <> b2 ; :: thesis: contradiction
hence contradiction by A9, A11, A17, A25, A145, AFF_1:39; :: thesis: verum
end;
A146: now
a2,a3 // a2,b3 by A21, A144, ANALMETR:81;
then LIN a2,a3,b3 by ANALMETR:def 11;
then LIN a2',a3',b3' by ANALMETR:55;
then A147: LIN a3',b3',a2' by AFF_1:15;
assume a3 <> b3 ; :: thesis: contradiction
hence contradiction by A6, A8, A14, A24, A147, AFF_1:39; :: thesis: verum
end;
assume ( a2 <> b2 or a3 <> b3 or a4 <> b4 ) ; :: thesis: contradiction
hence contradiction by A144, A142, A146; :: thesis: verum
end;
now
assume a1 = b1 ; :: thesis: a3,a4 // b3,b4
then a3',a4' // b3',b4' by A140, AFF_1:11;
hence a3,a4 // b3,b4 by ANALMETR:48; :: thesis: verum
end;
hence a3,a4 // b3,b4 by A31; :: thesis: verum