let x be set ; :: thesis: for G being Group

for H1, H2 being Subgroup of G st G is commutative Group holds

( x in H1 "\/" H2 iff ex a, b being Element of G st

( x = a * b & a in H1 & b in H2 ) )

let G be Group; :: thesis: for H1, H2 being Subgroup of G st G is commutative Group holds

( x in H1 "\/" H2 iff ex a, b being Element of G st

( x = a * b & a in H1 & b in H2 ) )

let H1, H2 be Subgroup of G; :: thesis: ( G is commutative Group implies ( x in H1 "\/" H2 iff ex a, b being Element of G st

( x = a * b & a in H1 & b in H2 ) ) )

assume G is commutative Group ; :: thesis: ( x in H1 "\/" H2 iff ex a, b being Element of G st

( x = a * b & a in H1 & b in H2 ) )

then H1 * H2 = H2 * H1 by GROUP_2:25;

hence ( x in H1 "\/" H2 iff ex a, b being Element of G st

( x = a * b & a in H1 & b in H2 ) ) by Th5; :: thesis: verum

for H1, H2 being Subgroup of G st G is commutative Group holds

( x in H1 "\/" H2 iff ex a, b being Element of G st

( x = a * b & a in H1 & b in H2 ) )

let G be Group; :: thesis: for H1, H2 being Subgroup of G st G is commutative Group holds

( x in H1 "\/" H2 iff ex a, b being Element of G st

( x = a * b & a in H1 & b in H2 ) )

let H1, H2 be Subgroup of G; :: thesis: ( G is commutative Group implies ( x in H1 "\/" H2 iff ex a, b being Element of G st

( x = a * b & a in H1 & b in H2 ) ) )

assume G is commutative Group ; :: thesis: ( x in H1 "\/" H2 iff ex a, b being Element of G st

( x = a * b & a in H1 & b in H2 ) )

then H1 * H2 = H2 * H1 by GROUP_2:25;

hence ( x in H1 "\/" H2 iff ex a, b being Element of G st

( x = a * b & a in H1 & b in H2 ) ) by Th5; :: thesis: verum