let A, X be set ; :: thesis: (delta X) " [:A,A:] c= A
set f = delta X;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (delta X) " [:A,A:] or x in A )
assume x in (delta X) " [:A,A:] ; :: thesis: x in A
then ( (delta X) . x in [:A,A:] & (delta X) . x = [x,x] ) by FUNCT_1:def 7, FUNCT_3:def 6;
hence x in A by ZFMISC_1:87; :: thesis: verum