let X, Y be set ; :: thesis: ( [:X,X,X,X,X,X,X,X,X:] = [:Y,Y,Y,Y,Y,Y,Y,Y,Y:] implies X = Y )
assume [:X,X,X,X,X,X,X,X,X:] = [:Y,Y,Y,Y,Y,Y,Y,Y,Y:] ; :: thesis: X = Y
then ( ( X <> {} or Y <> {} ) implies X = Y ) by Th62;
hence X = Y ; :: thesis: verum