let R be Relation; :: thesis: field (R [*]) = field R
set LH = field (R [*]);
set RH = field R;
B0: field R c= field (R [*]) by LANG1:18, RELAT_1:31;
field (R [*]) c= field R by Lm32;
hence field (R [*]) = field R by XBOOLE_0:def 10, B0; :: thesis: verum