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