let x, y be set ; :: according to RELAT_2:def 4,RELAT_2:def 12 :: thesis: ( not x in field ((f * R) * (f " )) or not y in field ((f * R) * (f " )) or not [x,y] in (f * R) * (f " ) or not [y,x] in (f * R) * (f " ) or x = y )
assume ( x in field ((f * R) * (f " )) & y in field ((f * R) * (f " )) ) ; :: thesis: ( not [x,y] in (f * R) * (f " ) or not [y,x] in (f * R) * (f " ) or x = y )
assume ( [x,y] in (f * R) * (f " ) & [y,x] in (f * R) * (f " ) ) ; :: thesis: x = y
then A1: ( x in dom f & y in dom f & [(f . x),(f . y)] in R & [(f . y),(f . x)] in R ) by Th6;
then ( f . x in field R & f . y in field R & R is_antisymmetric_in field R ) by RELAT_1:30, RELAT_2:def 12;
then f . x = f . y by A1, RELAT_2:def 4;
hence x = y by A1, FUNCT_1:def 8; :: thesis: verum