theorem Th16: :: YELLOW10:16

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