let M1, M2 be Subset of (Q. I); :: thesis: ( ( for z being Element of Q. I holds
( z in M1 iff (z `1) * (u `2) = (z `2) * (u `1) ) ) & ( for z being Element of Q. I holds
( z in M2 iff (z `1) * (u `2) = (z `2) * (u `1) ) ) implies M1 = M2 )
assume A2: for z being Element of Q. I holds
( z in M1 iff (z `1) * (u `2) = (z `2) * (u `1) ) ; :: thesis: ( ex z being Element of Q. I st
( ( z in M2 implies (z `1) * (u `2) = (z `2) * (u `1) ) implies ( (z `1) * (u `2) = (z `2) * (u `1) & not z in M2 ) ) or M1 = M2 )
assume A3: for z being Element of Q. I holds
( z in M2 iff (z `1) * (u `2) = (z `2) * (u `1) ) ; :: thesis: M1 = M2
A4: for x being object st x in M2 holds
x in M1
proof
let x be object ; :: thesis: ( x in M2 implies x in M1 )
assume A5: x in M2 ; :: thesis: x in M1
then reconsider x = x as Element of Q. I ;
(x `1) * (u `2) = (x `2) * (u `1) by A3, A5;
hence x in M1 by A2; :: thesis: verum
end;
for x being object st x in M1 holds
x in M2
proof
let x be object ; :: thesis: ( x in M1 implies x in M2 )
assume A6: x in M1 ; :: thesis: x in M2
then reconsider x = x as Element of Q. I ;
(x `1) * (u `2) = (x `2) * (u `1) by A2, A6;
hence x in M2 by A3; :: thesis: verum
end;
hence M1 = M2 by A4, TARSKI:2; :: thesis: verum