theorem :: TEX_4:36

for Y being non empty TopStruct
for A, B being Subset of Y holds MaxADSet (A \/ B) = (MaxADSet A) \/ (MaxADSet B)