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