let X be set ; :: thesis: for A being Subset of X holds (id X) " A = A
let A be Subset of X; :: thesis: (id X) " A = A
thus A = (id X) " ((id X) .: A) by Th61
.= (id X) " A by FUNCT_1:92 ; :: thesis: verum