the
carrier
of
[:
X
,
Y
:]
=
[:
the
carrier
of
X
, the
carrier
of
Y
:]
by
Def2
;
hence
.:
(
pr1
( the
carrier
of
X
, the
carrier
of
Y
)
)
is
Function
of
(
bool
the
carrier
of
[:
X
,
Y
:]
)
,
(
bool
the
carrier
of
X
)
;
:: thesis:
verum