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:16;
field (R [*]) c= field R by Lm32;
hence field (R [*]) = field R by B0, XBOOLE_0:def 10; :: thesis: verum