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

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

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
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;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