thus BCI_S-EXAMPLE is being_B :: thesis: ( BCI_S-EXAMPLE is being_C & BCI_S-EXAMPLE is being_I & BCI_S-EXAMPLE is being_BCI-4 & BCI_S-EXAMPLE is being_BCK-5 & BCI_S-EXAMPLE is with_condition_S )

proof

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

end;

thus BCI_S-EXAMPLE is being_C :: thesis: ( BCI_S-EXAMPLE is being_I & BCI_S-EXAMPLE is being_BCI-4 & BCI_S-EXAMPLE is being_BCK-5 & BCI_S-EXAMPLE is with_condition_S )

proof

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

end;

thus BCI_S-EXAMPLE is being_I :: thesis: ( BCI_S-EXAMPLE is being_BCI-4 & BCI_S-EXAMPLE is being_BCK-5 & BCI_S-EXAMPLE is with_condition_S )

proof

let x be Element of BCI_S-EXAMPLE ; :: according to BCIALG_1:def 5 :: thesis: x \ x = 0. BCI_S-EXAMPLE
thus x \ x = 0. BCI_S-EXAMPLE by STRUCT_0:def 10; :: thesis: verum

end;

thus BCI_S-EXAMPLE is being_BCI-4 :: thesis: ( BCI_S-EXAMPLE is being_BCK-5 & BCI_S-EXAMPLE is with_condition_S )

proof

let x, y be Element of BCI_S-EXAMPLE ; :: according to BCIALG_1:def 7 :: thesis: ( not x \ y = 0. BCI_S-EXAMPLE or not y \ x = 0. BCI_S-EXAMPLE or x = y )
thus ( not x \ y = 0. BCI_S-EXAMPLE or not y \ x = 0. BCI_S-EXAMPLE or x = y ) by STRUCT_0:def 10; :: thesis: verum

end;

thus BCI_S-EXAMPLE is being_BCK-5 :: thesis: BCI_S-EXAMPLE is with_condition_S

proof

let x be Element of BCI_S-EXAMPLE ; :: according to BCIALG_1:def 8 :: thesis: x ` = 0. BCI_S-EXAMPLE
thus x ` = 0. BCI_S-EXAMPLE by STRUCT_0:def 10; :: thesis: verum

end;

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