theorem :: YELLOW10:56

for S, T being non empty reflexive antisymmetric up-complete RelStr
for X being Subset of [:S,T:] st X is inaccessible holds
( proj1 X is inaccessible & proj2 X is inaccessible )