set X = { H where H is Element of Subgroups G : ex P being strict Subgroup of G st
( P = H & P is_Sylow_p-subgroup_of_prime p ) } ;

now :: thesis: for x being object st x in { H where H is Element of Subgroups G : ex P being strict Subgroup of G st
( P = H & P is_Sylow_p-subgroup_of_prime p ) } holds
x in Subgroups G

let x be object ; :: thesis: ( x in { H where H is Element of Subgroups G : ex P being strict Subgroup of G st
( P = H & P is_Sylow_p-subgroup_of_prime p ) } implies x in Subgroups G )
assume x in { H where H is Element of Subgroups G : ex P being strict Subgroup of G st
( P = H & P is_Sylow_p-subgroup_of_prime p ) } ; :: thesis: x in Subgroups G
then ex H being Element of Subgroups G st
( x = H & ex P being strict Subgroup of G st
( P = H & P is_Sylow_p-subgroup_of_prime p ) ) ;
hence x in Subgroups G ; :: thesis: verum

end;

hence { H where H is Element of Subgroups G : ex P being strict Subgroup of G st
( P = H & P is_Sylow_p-subgroup_of_prime p ) } is Subset of (Subgroups G) by TARSKI:def 3; :: thesis: verum