set
A
= the
Subset
of
U
;
set
IT
=
{
the
Subset
of
U
}
;
{
the
Subset
of
U
}
=
Inter
( the
Subset
of
U
, the
Subset
of
U
)
by
Th8
;
hence
ex
b
_{1}
being
Subset-Family
of
U
ex
A
,
B
being
Subset
of
U
st
b
_{1}
=
Inter
(
A
,
B
) ;
:: thesis:
verum