theorem Th41: :: YELLOW10:41

for S, T being non empty RelStr
for x being Element of [:S,T:] holds
( proj1 (uparrow x) c= uparrow (x `1) & proj2 (uparrow x) c= uparrow (x `2) )