let A be set ; :: thesis: for R being Relation st A c= R holds
A is Relation-like
let R be Relation; :: thesis: ( A c= R implies A is Relation-like )
assume A1: for x being set st x in A holds
x in R ; :: according to TARSKI:def 3 :: thesis: A is Relation-like
thus for x being set st x in A holds
ex y, z being set st x = [y,z] :: according to RELAT_1:def 1 :: thesis: verum

proof

let x be set ; :: thesis: ( x in A implies ex y, z being set st x = [y,z] )
assume x in A ; :: thesis: ex y, z being set st x = [y,z]
then x in R by A1;
hence ex y, z being set st x = [y,z] by Def1; :: thesis: verum

end;