take
[#]
L
;
:: thesis:
( not
[#]
L
is
empty
&
[#]
L
is
directed
&
[#]
L
is
filtered
&
[#]
L
is
lower
&
[#]
L
is
upper
)
thus
( not
[#]
L
is
empty
&
[#]
L
is
directed
&
[#]
L
is
filtered
&
[#]
L
is
lower
&
[#]
L
is
upper
) ;
:: thesis:
verum