let A, X be set ; :: thesis: (delta X) .: A c= [:A,A:]
set f = delta X;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (delta X) .: A or y in [:A,A:] )
assume y in (delta X) .: A ; :: thesis: y in [:A,A:]
then consider x being object such that
A1: x in dom (delta X) and
A2: x in A and
A3: y = (delta X) . x by FUNCT_1:def 6;
y = [x,x] by A1, A3, FUNCT_3:def 6;
hence y in [:A,A:] by A2, ZFMISC_1:def 2; :: thesis: verum