let x be set ; :: thesis: for R being Relation st x in R holds
x = [(x `1 ),(x `2 )]
let R be Relation; :: thesis: ( x in R implies x = [(x `1 ),(x `2 )] )
assume x in R ; :: thesis: x = [(x `1 ),(x `2 )]
then ex x1, x2 being set st x = [x1,x2] by RELAT_1:def 1;
hence x = [(x `1 ),(x `2 )] by Th8; :: thesis: verum