set H = { x where x is Element of F_Complex : x is CRoot of n, 1_ F_Complex } ;
for x being object st x in { x where x is Element of F_Complex : x is CRoot of n, 1_ F_Complex } holds
x in the carrier of F_Complex

proof

let x be object ; :: thesis: ( x in { x where x is Element of F_Complex : x is CRoot of n, 1_ F_Complex } implies x in the carrier of F_Complex )
assume x in { x where x is Element of F_Complex : x is CRoot of n, 1_ F_Complex } ; :: thesis: x in the carrier of F_Complex
then ex y being Element of F_Complex st
( y = x & y is CRoot of n, 1_ F_Complex ) ;
hence x in the carrier of F_Complex ; :: thesis: verum

end;

hence { x where x is Element of F_Complex : x is CRoot of n, 1_ F_Complex } is Subset of F_Complex by TARSKI:def 3; :: thesis: verum