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 Th100, Th101;
hence Y1 |` P1 c= Y2 |` P2 by XBOOLE_1:1; :: thesis: verum