theorem :: YELLOW10:49

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