let Y be non empty set ; :: thesis: for PA, PB being a_partition of Y holds PA '\/' (PA '/\' PB) = PA
let PA, PB be a_partition of Y; :: thesis: PA '\/' (PA '/\' PB) = PA
A1: ( ERl (PA '\/' (PA '/\' PB)) = (ERl PA) "\/" (ERl (PA '/\' PB)) & (ERl PA) "\/" (ERl (PA '/\' PB)) = (ERl PA) "\/" ((ERl PA) /\ (ERl PB)) ) by Th27, Th28;
thus PA '\/' (PA '/\' PB) = PA by A1, Th29, EQREL_1:25; :: thesis: verum