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