let M1, M2 be Element of Quot. I; :: thesis: ( ( for z being Element of Q. I holds
( z in M1 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) ) ) & ( for z being Element of Q. I holds
( z in M2 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) ) ) implies M1 = M2 )
assume A12: for z being Element of Q. I holds
( z in M1 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) ) ; :: thesis: ( ex z being Element of Q. I st
( ( z in M2 implies ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) ) implies ( ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) & not z in M2 ) ) or M1 = M2 )
assume A13: for z being Element of Q. I holds
( z in M2 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) ) ; :: thesis: M1 = M2
A14: for z being Element of Q. I st z in M2 holds
z in M1

proof

let z be Element of Q. I; :: thesis: ( z in M2 implies z in M1 )
assume z in M2 ; :: thesis: z in M1
then ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) by A13;
hence z in M1 by A12; :: thesis: verum

end;

for z being Element of Q. I st z in M1 holds
z in M2

proof

let z be Element of Q. I; :: thesis: ( z in M1 implies z in M2 )
assume z in M1 ; :: thesis: z in M2
then ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) by A12;
hence z in M2 by A13; :: thesis: verum

end;

hence M1 = M2 by A14, SUBSET_1:3; :: thesis: verum