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