theorem Th22: :: YELLOW10:22

for S, T being non empty reflexive antisymmetric up-complete RelStr
for x being Element of [:S,T:] st x is compact holds
( x `1 is compact & x `2 is compact )