set IT = BCI-EXAMPLE ;
thus BCI-EXAMPLE is BCI-commutative :: thesis: BCI-EXAMPLE is BCI-weakly-commutative

proof

let x, y be Element of BCI-EXAMPLE; :: according to BCIALG_3:def 4 :: thesis: ( x \ y = 0. BCI-EXAMPLE implies x = y \ (y \ x) )
thus ( x \ y = 0. BCI-EXAMPLE implies x = y \ (y \ x) ) by STRUCT_0:def 10; :: thesis: verum

end;

let x, y be Element of BCI-EXAMPLE; :: according to BCIALG_3:def 5 :: thesis: (x \ (x \ y)) \ ((0. BCI-EXAMPLE) \ (x \ y)) = y \ (y \ x)
thus (x \ (x \ y)) \ ((0. BCI-EXAMPLE) \ (x \ y)) = y \ (y \ x) by STRUCT_0:def 10; :: thesis: verum