set M = { z where z is Element of Q. I : (z `1) * (u `2) = (z `2) * (u `1) } ;
for x being Element of Q. I st x in { z where z is Element of Q. I : (z `1) * (u `2) = (z `2) * (u `1) } holds
(x `1) * (u `2) = (x `2) * (u `1)

proof

let x be Element of Q. I; :: thesis: ( x in { z where z is Element of Q. I : (z `1) * (u `2) = (z `2) * (u `1) } implies (x `1) * (u `2) = (x `2) * (u `1) )
assume x in { z where z is Element of Q. I : (z `1) * (u `2) = (z `2) * (u `1) } ; :: thesis: (x `1) * (u `2) = (x `2) * (u `1)
then ex z being Element of Q. I st
( x = z & (z `1) * (u `2) = (z `2) * (u `1) ) ;
hence (x `1) * (u `2) = (x `2) * (u `1) ; :: thesis: verum

end;

then A1: for x being Element of Q. I holds
( x in { z where z is Element of Q. I : (z `1) * (u `2) = (z `2) * (u `1) } iff (x `1) * (u `2) = (x `2) * (u `1) ) ;
for x being object st x in { z where z is Element of Q. I : (z `1) * (u `2) = (z `2) * (u `1) } holds
x in Q. I

proof

let x be object ; :: thesis: ( x in { z where z is Element of Q. I : (z `1) * (u `2) = (z `2) * (u `1) } implies x in Q. I )
assume x in { z where z is Element of Q. I : (z `1) * (u `2) = (z `2) * (u `1) } ; :: thesis: x in Q. I
then ex z being Element of Q. I st
( x = z & (z `1) * (u `2) = (z `2) * (u `1) ) ;
hence x in Q. I ; :: thesis: verum

end;

then { z where z is Element of Q. I : (z `1) * (u `2) = (z `2) * (u `1) } is Subset of (Q. I) by TARSKI:def 3;
hence ex b₁ being Subset of (Q. I) st
for z being Element of Q. I holds
( z in b₁ iff (z `1) * (u `2) = (z `2) * (u `1) ) by A1; :: thesis: verum