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)
A1: ERl ((PA '\/' PB) '\/' PC) = (ERl (PA '\/' PB)) "\/" (ERl PC) by Th27
.= ((ERl PA) "\/" (ERl PB)) "\/" (ERl PC) by Th27
.= (ERl PA) "\/" ((ERl PB) "\/" (ERl PC)) by EQREL_1:21
.= (ERl PA) "\/" (ERl (PB '\/' PC)) by Th27
.= ERl (PA '\/' (PB '\/' PC)) by Th27 ;
thus (PA '\/' PB) '\/' PC = PA '\/' (PB '\/' PC) by A1, Th29; :: thesis: verum