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 set 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 set ; :: 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