set H3 = { x where x is Element of Q : ( x in H1 or x = 1. Q or S₁[Q,H2,x] ) } ;
{ x where x is Element of Q : ( x in H1 or x = 1. Q or S₁[Q,H2,x] ) } 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 : ( x in H1 or x = 1. Q or S₁[Q,H2,x] ) } or x in the carrier of Q )
assume x in { x where x is Element of Q : ( x in H1 or x = 1. Q or S₁[Q,H2,x] ) } ; :: thesis: x in the carrier of Q
then ex x1 being Element of Q st
( x = x1 & ( x1 in H1 or x1 = 1. Q or S₁[Q,H2,x1] ) ) ;
hence x in the carrier of Q ; :: thesis: verum

end;

then reconsider H3 = { x where x is Element of Q : ( x in H1 or x = 1. Q or S₁[Q,H2,x] ) } as Subset of Q ;
take H3 ; :: 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 ) ) ) )
let x be Element of Q; :: thesis: ( 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 ) ) ) )
thus ( not x in H3 or x in H1 or x = 1. Q or S₁[Q,H2,x] ) :: thesis: ( ( 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 x in H3 )

proof

assume x in H3 ; :: thesis: ( x in H1 or x = 1. Q or S₁[Q,H2,x] )
then ex x1 being Element of Q st
( x = x1 & ( x1 in H1 or x1 = 1. Q or S₁[Q,H2,x1] ) ) ;
hence ( x in H1 or x = 1. Q or S₁[Q,H2,x] ) ; :: thesis: verum

end;

thus ( ( 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 x in H3 ) ; :: thesis: verum