set IT = BCI-EXAMPLE ;
consider a being Element of BCI-EXAMPLE ;
BCI-EXAMPLE is bounded

proof

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

end;

hence BCI-EXAMPLE is bounded ; :: thesis: verum