let p be Element of G; :: thesis: p is a_partition of Y
thus p is a_partition of Y by PARTIT1:def 3; :: thesis: verum