set
x
= the
set
;
set
R
= the
Order
of
{
the
set
}
;
RelStr
(#
{
the
set
}
, the
Order
of
{
the
set
}
#) is 1
-element
RelStr
;
hence
ex
b
_{1}
being
LATTICE
st
b
_{1}
is
completely-distributive
;
:: thesis:
verum