the
carrier
of
[:
X
,
Y
:]
=
[:
the
carrier
of
X
, the
carrier
of
Y
:]
by
Def2
;
hence
not the
carrier
of
[:
X
,
Y
:]
is
empty
;
:: according to
STRUCT_0:def 1
:: thesis:
verum