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 A1: ( PA '>' PC & PB '>' PC ) ; :: thesis: PA '/\' PB '>' PC
A2: ( ERl PC c= ERl PA & ERl PC c= ERl PB ) by A1, Th24;
A3: ERl (PA '/\' PB) = (ERl PA) /\ (ERl PB) by Th28;
A4: ERl PC c= ERl (PA '/\' PB) by A2, A3, XBOOLE_1:19;
thus PA '/\' PB '>' PC by A4, Th24; :: thesis: verum