theorem Lm56: :: ALGNUM_1:45

for x being Element of F_Complex holds
( [:RAT,RAT:] c= [:(FQ x),(FQ x):] & [:(FQ x),(FQ x):] c= [:COMPLEX,COMPLEX:] )