let R be Relation; :: thesis: field (R [*]) c= field R
set RR = R [*] ;
set LH = field (R [*]);
set RH = field R;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in field (R [*]) or x in field R )
assume A1: x in field (R [*]) ; :: thesis: x in field R
per cases ( x in dom (R [*]) or x in rng (R [*]) ) by A1, XBOOLE_0:def 3;
suppose x in dom (R [*]) ; :: thesis: x in field R
then consider y being object such that
A2: [x,y] in R [*] by XTUPLE_0:def 12;
thus x in field R by A2, FINSEQ_1:def 16; :: thesis: verum
end;
suppose x in rng (R [*]) ; :: thesis: x in field R
then consider y being object such that
A3: [y,x] in R [*] by XTUPLE_0:def 13;
thus x in field R by FINSEQ_1:def 16, A3; :: thesis: verum
end;
end;