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 `2) = (z `2) * (- (a `1)) ) ) ) & ( 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 `2) = (z `2) * (- (a `1)) ) ) ) implies M1 = M2 )
assume A10: 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 `2) = (z `2) * (- (a `1)) ) ) ; :: 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 `2) = (z `2) * (- (a `1)) ) ) implies ( ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) & not z in M2 ) ) or M1 = M2 )
assume A11: 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 `2) = (z `2) * (- (a `1)) ) ) ; :: thesis: M1 = M2
A12: 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 `2) = (z `2) * (- (a `1)) ) by A11;
hence z in M1 by A10; :: 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 `2) = (z `2) * (- (a `1)) ) by A10;
hence z in M2 by A11; :: thesis: verum

end;

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