theorem Th51: :: YELLOW10:51

for S, T being non empty reflexive antisymmetric up-complete RelStr
for x being Element of [:S,T:] holds
( proj1 (compactbelow x) c= compactbelow (x `1) & proj2 (compactbelow x) c= compactbelow (x `2) )