let T be 1-sorted ; :: thesis: for P being Subset of holds P \/ (P ` ) = [#] T
let P be Subset of ; :: thesis: P \/ (P ` ) = [#] T
P \/ (P ` ) = [#] the carrier of T by SUBSET_1:25
.= the carrier of T ;
hence P \/ (P ` ) = [#] T ; :: thesis: verum