:: deftheorem defines |_2 WELLORD1:def 6 :
for R being Relation
for Y being set holds R |_2 Y = R /\ [:Y,Y:];