let H31, H32 be Subset of Q; :: thesis: ( ( for x being Element of Q holds
( x in H31 iff ex y, z being Element of Q st
( y in H1 & z in H2 & x = y \ z ) ) ) & ( for x being Element of Q holds
( x in H32 iff ex y, z being Element of Q st
( y in H1 & z in H2 & x = y \ z ) ) ) implies H31 = H32 )
assume that
A5: for x being Element of Q holds
( x in H31 iff ex y, z being Element of Q st
( y in H1 & z in H2 & x = y \ z ) ) and
A6: for x being Element of Q holds
( x in H32 iff ex y, z being Element of Q st
( y in H1 & z in H2 & x = y \ z ) ) ; :: thesis: H31 = H32

now :: thesis: for x being Element of Q holds
( x in H31 iff x in H32 )

let x be Element of Q; :: thesis: ( x in H31 iff x in H32 )
( x in H31 iff ex y, z being Element of Q st
( y in H1 & z in H2 & x = y \ z ) ) by A5;
hence ( x in H31 iff x in H32 ) by A6; :: thesis: verum

end;

hence H31 = H32 by SUBSET_1:3; :: thesis: verum