set IT = BCI-EXAMPLE ;
set a = the Element of BCI-EXAMPLE;
BCI-EXAMPLE is bounded
proof
take the Element of BCI-EXAMPLE ; :: according to BCIALG_3:def 6 :: thesis: the Element of BCI-EXAMPLE is being_greatest
for x being Element of BCI-EXAMPLE holds x \ the Element of BCI-EXAMPLE = 0. BCI-EXAMPLE by STRUCT_0:def 10;
hence the Element of BCI-EXAMPLE is being_greatest ; :: thesis: verum
end;
hence BCI-EXAMPLE is bounded ; :: thesis: verum