theorem Th27: :: WAYBEL30:27

for N being non empty reflexive RelStr
for X, Y being Subset of N holds (X ^0) \/ (Y ^0) c= (X \/ Y) ^0