theorem Th24: :: YELLOW10:24

for S, T being antisymmetric with_infima RelStr
for X, Y being Subset of [:S,T:] holds
( proj1 (X "/\" Y) = (proj1 X) "/\" (proj1 Y) & proj2 (X "/\" Y) = (proj2 X) "/\" (proj2 Y) )