let Y be non empty set ; :: thesis: for PA, PB, PC being a_partition of Y st PA '>' PC & PB '>' PC holds
PA '/\' PB '>' PC
let PA, PB, PC be a_partition of Y; :: thesis: ( PA '>' PC & PB '>' PC implies PA '/\' PB '>' PC )
assume ( PA '>' PC & PB '>' PC ) ; :: thesis: PA '/\' PB '>' PC
then A1: ( ERl PC c= ERl PA & ERl PC c= ERl PB ) by Th20;
ERl (PA '/\' PB) = (ERl PA) /\ (ERl PB) by Th24;
then ERl PC c= ERl (PA '/\' PB) by A1, XBOOLE_1:19;
hence PA '/\' PB '>' PC by Th20; :: thesis: verum