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