for E being Field
for F being Subfield of E
for x being non zero Element of E
for x1 being Element of F st x = x1 holds
x " = x1 "