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 b1 being Subset of (Q. I) st
for z being Element of Q. I holds
( z in b1 iff (z `1) * (u `2) = (z `2) * (u `1) ) by A1; :: thesis: verum