let Y1, Y2 be set ; :: thesis: for P1, P2 being Relation st P1 c= P2 & Y1 c= Y2 holds
Y1 | P1 c= Y2 | P2
let P1, P2 be Relation; :: thesis: ( P1 c= P2 & Y1 c= Y2 implies Y1 | P1 c= Y2 | P2 )
assume ( P1 c= P2 & Y1 c= Y2 ) ; :: thesis: Y1 | P1 c= Y2 | P2
then ( Y1 | P1 c= Y1 | P2 & Y1 | P2 c= Y2 | P2 ) by Th131, Th132;
hence Y1 | P1 c= Y2 | P2 by XBOOLE_1:1; :: thesis: verum