let X be set ; :: thesis: for R being Relation holds
( field (R |_2 X) c= field R & field (R |_2 X) c= X )
let R be Relation; :: thesis: ( field (R |_2 X) c= field R & field (R |_2 X) c= X )
( ( for x being set st x in field (R |_2 X) holds
x in field R ) & ( for x being set st x in field (R |_2 X) holds
x in X ) ) by Th19;
hence ( field (R |_2 X) c= field R & field (R |_2 X) c= X ) by TARSKI:def 3; :: thesis: verum