theorem Th15: :: YELLOW10:15

for S, T being antisymmetric with_infima RelStr
for x1, y1 being Element of S
for x2, y2 being Element of T holds [(x1 "/\" y1),(x2 "/\" y2)] = [x1,x2] "/\" [y1,y2]