let X, Y be set ; :: thesis: X ++ Y = Y ++ X
( X ++ Y c= Y ++ X & Y ++ X c= X ++ Y ) by Lm4;
hence X ++ Y = Y ++ X by XBOOLE_0:def 10; :: thesis: verum