let P, R be Relation; :: thesis: ( P c= R implies field P c= field R )
assume P c= R ; :: thesis: field P c= field R
then ( dom P c= dom R & rng P c= rng R ) by XTUPLE_0:8, XTUPLE_0:9;
hence field P c= field R by XBOOLE_1:13; :: thesis: verum