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