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