set IT = BCI-EXAMPLE ;
A1: BCI-EXAMPLE is implicative

proof

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

end;

A2: BCI-EXAMPLE is positive-implicative

proof

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

end;

A3: BCI-EXAMPLE is p-Semisimple

proof

let x, y be Element of BCI-EXAMPLE ; :: according to BCIALG_1:def 26 :: thesis: x \ (x \ y) = y
( x \ (x \ y) = {} & {} = y ) by CARD_1:87, TARSKI:def 1;
hence x \ (x \ y) = y ; :: thesis: verum

end;

A4: BCI-EXAMPLE is associative

proof

let x, y, z be Element of BCI-EXAMPLE ; :: according to BCIALG_1:def 20 :: thesis: (x \ y) \ z = x \ (y \ z)
( (x \ y) \ z = {} & x \ (y \ z) = {} ) by CARD_1:87, TARSKI:def 1;
hence (x \ y) \ z = x \ (y \ z) ; :: thesis: verum

end;

A5: BCI-EXAMPLE is weakly-implicative

proof

let x, y be Element of BCI-EXAMPLE ; :: according to BCIALG_1:def 25 :: thesis: (x \ (y \ x)) \ ((y \ x) ` ) = x
( (x \ (y \ x)) \ ((y \ x) ` ) = {} & x = {} ) by CARD_1:87, TARSKI:def 1;
hence (x \ (y \ x)) \ ((y \ x) ` ) = x ; :: thesis: verum

end;

BCI-EXAMPLE is weakly-positive-implicative

proof

let x, y, z be Element of BCI-EXAMPLE ; :: according to BCIALG_1:def 23 :: thesis: (x \ y) \ z = ((x \ z) \ z) \ (y \ z)
thus (x \ y) \ z = ((x \ z) \ z) \ (y \ z) by STRUCT_0:def 10; :: thesis: verum

end;

hence ( BCI-EXAMPLE is implicative & BCI-EXAMPLE is positive-implicative & BCI-EXAMPLE is p-Semisimple & BCI-EXAMPLE is associative & BCI-EXAMPLE is weakly-implicative & BCI-EXAMPLE is weakly-positive-implicative ) by A1, A2, A3, A4, A5; :: thesis: verum