let
A
,
B
be
set
;
:: according to
FINSUB_1:def 2
:: thesis:
( not
A
in
bool
X
or not
B
in
bool
X
or
A
/\
B
in
bool
X
)
assume
that
A1
:
A
in
bool
X
and
B
in
bool
X
;
:: thesis:
A
/\
B
in
bool
X
A
/\
B
c=
X
by
A1
,
XBOOLE_1:108
;
hence
A
/\
B
in
bool
X
;
:: thesis:
verum