let Y be set ; :: thesis: for P1, P2 being Relation st P1 c= P2 holds
Y |` P1 c= Y |` P2
let P1, P2 be Relation; :: thesis: ( P1 c= P2 implies Y |` P1 c= Y |` P2 )
assume A1: P1 c= P2 ; :: thesis: Y |` P1 c= Y |` P2
let x be set ; :: according to RELAT_1:def 3 :: thesis: for b being set st [x,b] in Y |` P1 holds
[x,b] in Y |` P2
let y be set ; :: thesis: ( [x,y] in Y |` P1 implies [x,y] in Y |` P2 )
assume [x,y] in Y |` P1 ; :: thesis: [x,y] in Y |` P2
then ( [x,y] in P1 & y in Y ) by Def12;
hence [x,y] in Y |` P2 by A1, Def12; :: thesis: verum