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 PA c= ERl PC & ERl PB c= ERl PC ) by A1, Th24;
A3: ERl (PA '\/' PB) = (ERl PA) "\/" (ERl PB) by Th27;
A4: (ERl PA) \/ (ERl PB) c= ERl PC by A2, XBOOLE_1:8;
A5: (ERl PA) "\/" (ERl PB) c= ERl PC by A4, EQREL_1:def 3;
thus PA '\/' PB '<' PC by A3, A5, Th24; :: thesis: verum