Definition 1.1.27.  Let S be a set. We define:
P(S) :=: {(T) | T ⊆ S}
(T) = (T')  :⇔  T = T'  (T ⊆ S, T' ⊆ S)
For S' ⊆ S, we canonically treat elements of P(S') as elements of P(S).
Remarks.

The power set is another example of a construction. It is slightly nonstandard in that its elements are not actual subsets but terms that are built using the constructor of this construction. To highlight this difference, parentheses are used. There is no significant practical difference, however.

References.