let A be set ; :: thesis: (delta A) ~ = delta A
thus (delta A) ~ = <:(id A),(id A):> ~ by Th1
.= <:(id A),(id A):> by Th2
.= delta A by Th1 ; :: thesis: verum