let H3, H4 be Subset of Q; :: thesis: ( ( for x being Element of Q holds
( x in H3 iff ( x in H1 or x = 1. Q or ex y, z being Element of Q st
( y in H2 & z in H2 & ( x = y * z or x = y \ z or x = y / z ) ) ) ) ) & ( for x being Element of Q holds
( x in H4 iff ( x in H1 or x = 1. Q or ex y, z being Element of Q st
( y in H2 & z in H2 & ( x = y * z or x = y \ z or x = y / z ) ) ) ) ) implies H3 = H4 )
assume that
A1: for x being Element of Q holds
( x in H3 iff ( x in H1 or x = 1. Q or S1[Q,H2,x] ) ) and
A2: for x being Element of Q holds
( x in H4 iff ( x in H1 or x = 1. Q or S1[Q,H2,x] ) ) ; :: thesis: H3 = H4
now :: thesis: for x being Element of Q holds
( x in H3 iff x in H4 )
let x be Element of Q; :: thesis: ( x in H3 iff x in H4 )
( x in H3 iff ( x in H1 or x = 1. Q or S1[Q,H2,x] ) ) by A1;
hence ( x in H3 iff x in H4 ) by A2; :: thesis: verum
end;
hence H3 = H4 by SUBSET_1:3; :: thesis: verum