let R be Relation; :: thesis: field R = field (R ~)
thus field R = (rng (R ~)) \/ (rng R) by Th20
.= field (R ~) by Th20 ; :: thesis: verum