theorem Th3: :: MMLQUER2:3

for X, Y being set holds (id X) .: Y = X /\ Y