M
c=
M
;
hence
( (
B
<>
{}
implies
meet
B
is
Subset
of
M
) & ( not
B
<>
{}
implies
M
is
Subset
of
M
) ) ;
:: thesis:
verum