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