let M1, M2 be Element of Quot. I; :: thesis: ( ( for z being Element of Q. I holds
( z in M1 iff z `1 = 0. I ) ) & ( for z being Element of Q. I holds
( z in M2 iff z `1 = 0. I ) ) implies M1 = M2 )
assume A3: for z being Element of Q. I holds
( z in M1 iff z `1 = 0. I ) ; :: thesis: ( ex z being Element of Q. I st
( ( z in M2 implies z `1 = 0. I ) implies ( z `1 = 0. I & not z in M2 ) ) or M1 = M2 )
assume A4: for z being Element of Q. I holds
( z in M2 iff z `1 = 0. I ) ; :: thesis: M1 = M2
A5: 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 z `1 = 0. I by A4;
hence z in M1 by A3; :: 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 z `1 = 0. I by A3;
hence z in M2 by A4; :: thesis: verum
end;
hence M1 = M2 by A5, SUBSET_1:3; :: thesis: verum