let y, x be Element of COMPLEX ; :: thesis: y .|. x = (x .|. y) *'
thus y .|. x = ((y * (x *' )) *' ) *'
.= (((x *' ) *' ) * (y *' )) *' by COMPLEX1:121
.= (x .|. y) *' ; :: thesis: verum