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