theorem :: WAYBEL30:24

for N being non empty reflexive RelStr
for A, J being Subset of N st A c= J holds
A ^0 c= J ^0