let x, y be object ; for R being Relation holds
( y in Class (R,x) iff [x,y] in R )
let R be Relation; ( y in Class (R,x) iff [x,y] in R )
thus
( y in Class (R,x) implies [x,y] in R )
( [x,y] in R implies y in Class (R,x) )
A1:
x in {x}
by TARSKI:def 1;
assume
[x,y] in R
; y in Class (R,x)
hence
y in Class (R,x)
by A1, RELAT_1:def 13; verum