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

proof

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

end;

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