set H3 = { x where x is Element of Q : ex y, z being Element of Q st
( y in H1 & z in H2 & x = y * z ) } ;
{ x where x is Element of Q : ex y, z being Element of Q st
( y in H1 & z in H2 & x = y * z ) } c= the carrier of Q

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Element of Q : ex y, z being Element of Q st
( y in H1 & z in H2 & x = y * z ) } or x in the carrier of Q )
assume x in { x where x is Element of Q : ex y, z being Element of Q st
( y in H1 & z in H2 & x = y * z ) } ; :: thesis: x in the carrier of Q
then ex x1 being Element of Q st
( x = x1 & ex y, z being Element of Q st
( y in H1 & z in H2 & x1 = y * z ) ) ;
hence x in the carrier of Q ; :: thesis: verum

end;

then reconsider H3 = { x where x is Element of Q : ex y, z being Element of Q st
( y in H1 & z in H2 & x = y * z ) } as Subset of Q ;
take H3 ; :: thesis: for x being Element of Q holds
( x in H3 iff ex y, z being Element of Q st
( y in H1 & z in H2 & x = y * z ) )
let x be Element of Q; :: thesis: ( x in H3 iff ex y, z being Element of Q st
( y in H1 & z in H2 & x = y * z ) )
( x in H3 implies ex y, z being Element of Q st
( y in H1 & z in H2 & x = y * z ) )

proof

assume x in H3 ; :: thesis: ex y, z being Element of Q st
( y in H1 & z in H2 & x = y * z )
then consider x1 being Element of Q such that
A1: ( x = x1 & ex y, z being Element of Q st
( y in H1 & z in H2 & x1 = y * z ) ) ;
thus ex y, z being Element of Q st
( y in H1 & z in H2 & x = y * z ) by A1; :: thesis: verum

end;

hence ( x in H3 iff ex y, z being Element of Q st
( y in H1 & z in H2 & x = y * z ) ) ; :: thesis: verum