let x be set ; :: according to RELAT_2:def 4,RELAT_2:def 12 :: thesis: for y being set st x in field (R ~) & y in field (R ~) & [x,y] in R ~ & [y,x] in R ~ holds
x = y
let y be set ; :: thesis: ( x in field (R ~) & y in field (R ~) & [x,y] in R ~ & [y,x] in R ~ implies x = y )
assume that
A2: ( x in field (R ~) & y in field (R ~) ) and
A3: ( [x,y] in R ~ & [y,x] in R ~ ) ; :: thesis: x = y
A4: ( [y,x] in R & [x,y] in R ) by A3, RELAT_1:def 7;
( x in field R & y in field R ) by A2, RELAT_1:21;
hence x = y by A4, Def4, Def12; :: thesis: verum