let x be Element of PA; :: thesis: x is Subset of
thus x is Subset of ; :: thesis: verum