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

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