let x, y be object ; :: 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:15;
then f . x = f . y by A6, A5, A4;
hence x = y by A3, FUNCT_1:def 4; :: thesis: verum