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