let X be set ; :: thesis: for A being Subset of X holds (delta X) " [:A,A:] = A
let A be Subset of X; :: thesis: (delta X) " [:A,A:] = A
set f = delta X;
thus (delta X) " [:A,A:] c= A by Th2; :: according to XBOOLE_0:def 10 :: thesis: A c= (delta X) " [:A,A:]
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in (delta X) " [:A,A:] )
assume A1: x in A ; :: thesis: x in (delta X) " [:A,A:]
then (delta X) . x = [x,x] by FUNCT_3:def 7;
then ( dom (delta X) = X & (delta X) . x in [:A,A:] ) by A1, FUNCT_3:def 7, ZFMISC_1:106;
hence x in (delta X) " [:A,A:] by A1, FUNCT_1:def 13; :: thesis: verum