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 that
x in field ((f * R) * (f " )) and
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 that
A1: [x,y] in (f * R) * (f " ) and
A2: [y,x] in (f * R) * (f " ) ; :: thesis: x = y
A3: ( x in dom f & y in dom f ) by A1, Th6;
A4: R is_antisymmetric_in field R by RELAT_2:def 12;
A5: [(f . y),(f . x)] in R by A2, Th6;
A6: [(f . x),(f . y)] in R by A1, Th6;
then ( f . x in field R & f . y in field R ) by RELAT_1:30;
then f . x = f . y by A6, A5, A4, RELAT_2:def 4;
hence x = y by A3, FUNCT_1:def 8; :: thesis: verum