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