let a, b be Nat; :: thesis: for m being non zero Nat st a,b are_coprime holds
Product (Sgm { q where q is Prime : ( q divides m & q divides b ) } ), Product (Sgm { r where r is Prime : ( r divides m & not r divides a & not r divides b ) } ) are_coprime
let m be non zero Nat; :: thesis: ( a,b are_coprime implies Product (Sgm { q where q is Prime : ( q divides m & q divides b ) } ), Product (Sgm { r where r is Prime : ( r divides m & not r divides a & not r divides b ) } ) are_coprime )
set A = { r where r is Prime : ( r divides m & not r divides a & not r divides b ) } ;
set B = { r where r is Prime : ( r divides m & not r divides b & not r divides a ) } ;
{ r where r is Prime : ( r divides m & not r divides a & not r divides b ) } = { r where r is Prime : ( r divides m & not r divides b & not r divides a ) }

proof

hereby :: according to XBOOLE_0:def 10,TARSKI:def 3 :: thesis: { r where r is Prime : ( r divides m & not r divides b & not r divides a ) } c= { r where r is Prime : ( r divides m & not r divides a & not r divides b ) }

let x be object ; :: thesis: ( x in { r where r is Prime : ( r divides m & not r divides a & not r divides b ) } implies x in { r where r is Prime : ( r divides m & not r divides b & not r divides a ) } )
assume x in { r where r is Prime : ( r divides m & not r divides a & not r divides b ) } ; :: thesis: x in { r where r is Prime : ( r divides m & not r divides b & not r divides a ) }
then ex r being Prime st
( x = r & r divides m & not r divides a & not r divides b ) ;
hence x in { r where r is Prime : ( r divides m & not r divides b & not r divides a ) } ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { r where r is Prime : ( r divides m & not r divides b & not r divides a ) } or x in { r where r is Prime : ( r divides m & not r divides a & not r divides b ) } )
assume x in { r where r is Prime : ( r divides m & not r divides b & not r divides a ) } ; :: thesis: x in { r where r is Prime : ( r divides m & not r divides a & not r divides b ) }
then ex r being Prime st
( x = r & r divides m & not r divides b & not r divides a ) ;
hence x in { r where r is Prime : ( r divides m & not r divides a & not r divides b ) } ; :: thesis: verum

end;

hence ( a,b are_coprime implies Product (Sgm { q where q is Prime : ( q divides m & q divides b ) } ), Product (Sgm { r where r is Prime : ( r divides m & not r divides a & not r divides b ) } ) are_coprime ) by Th14; :: thesis: verum