let Y be non empty set ; :: thesis: for PA, PB, PC being a_partition of Y holds (PA '\/' PB) '\/' PC = PA '\/' (PB '\/' PC)
let PA, PB, PC be a_partition of Y; :: thesis: (PA '\/' PB) '\/' PC = PA '\/' (PB '\/' PC)
ERl ((PA '\/' PB) '\/' PC) = (ERl (PA '\/' PB)) "\/" (ERl PC) by Th23
.= ((ERl PA) "\/" (ERl PB)) "\/" (ERl PC) by Th23
.= (ERl PA) "\/" ((ERl PB) "\/" (ERl PC)) by EQREL_1:13
.= (ERl PA) "\/" (ERl (PB '\/' PC)) by Th23
.= ERl (PA '\/' (PB '\/' PC)) by Th23 ;
hence (PA '\/' PB) '\/' PC = PA '\/' (PB '\/' PC) by Th25; :: thesis: verum