A0: ( 0 in {0,1,2} & 1 in {0,1,2} ) by ENUMSET1:def 1;
then QLT_Ex1 . (0,1) = 0 by QLTEx1Def;
hence QLT_Ex1 <> QLT_Ex2 by A0, QLTEx2Def; :: thesis: verum