set IT = BCI-EXAMPLE ;
BCI-EXAMPLE is Iseki_extension

proof

consider a being Element of BCI-EXAMPLE ;
take a ; :: according to BCIALG_3:def 9 :: thesis: a is being_Iseki
for x being Element of BCI-EXAMPLE holds
( x \ a = 0. BCI-EXAMPLE & a \ x = a ) by STRUCT_0:def 10;
hence a is being_Iseki by Def8; :: thesis: verum

end;

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