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 PA c= ERl PC & ERl PB c= ERl PC ) by Th20;
A2: ERl (PA '\/' PB) = (ERl PA) "\/" (ERl PB) by Th23;
(ERl PA) \/ (ERl PB) c= ERl PC by A1, XBOOLE_1:8;
then (ERl PA) "\/" (ERl PB) c= ERl PC by EQREL_1:def 2;
hence PA '\/' PB '<' PC by A2, Th20; :: thesis: verum