let x, y be Complex; :: thesis: y .|. x = (x .|. y) *'
thus y .|. x = ((y * (x *')) *') *'
.= (((x *') *') * (y *')) *' by COMPLEX1:35
.= (x .|. y) *' ; :: thesis: verum