thus BCI_S-EXAMPLE is being_SB-1 :: thesis: ( BCI_S-EXAMPLE is being_SB-2 & BCI_S-EXAMPLE is being_SB-4 & BCI_S-EXAMPLE is being_I & BCI_S-EXAMPLE is with_condition_S )

proof

let x be Element of BCI_S-EXAMPLE ; :: according to BCIALG_4:def 12 :: thesis: x * x = x
thus x * x = x by STRUCT_0:def 10; :: thesis: verum

end;

thus BCI_S-EXAMPLE is being_SB-2 :: thesis: ( BCI_S-EXAMPLE is being_SB-4 & BCI_S-EXAMPLE is being_I & BCI_S-EXAMPLE is with_condition_S )

proof

let x, y be Element of BCI_S-EXAMPLE ; :: according to BCIALG_4:def 13 :: thesis: x * y = y * x
thus x * y = y * x by STRUCT_0:def 10; :: thesis: verum

end;

thus BCI_S-EXAMPLE is being_SB-4 :: thesis: ( BCI_S-EXAMPLE is being_I & BCI_S-EXAMPLE is with_condition_S )

proof

let x, y be Element of BCI_S-EXAMPLE ; :: according to BCIALG_4:def 14 :: thesis: (x \ y) * y = x * y
thus (x \ y) * y = x * y by STRUCT_0:def 10; :: thesis: verum

end;

thus BCI_S-EXAMPLE is being_I ; :: thesis: BCI_S-EXAMPLE is with_condition_S
let x, y, z be Element of BCI_S-EXAMPLE ; :: according to BCIALG_4:def 2 :: thesis: (x \ y) \ z = x \ (y * z)
thus (x \ y) \ z = x \ (y * z) by STRUCT_0:def 10; :: thesis: verum