let U be non empty set ; :: thesis: (U -deltaInterpreter) " {1} = { <*u,u*> where u is Element of U : verum }
set RH = { <*u,u*> where u is Element of U : verum } ;
set LH = (U -deltaInterpreter) " {1};
set X = (U -concatenation) .: (id (1 -tuples_on U));
( (U -deltaInterpreter) " {1} = (U -concatenation) .: (id (1 -tuples_on U)) & (U -concatenation) .: (id (1 -tuples_on U)) = { <*u,u*> where u is Element of U : verum } ) by Lm26, FOMODEL0:38;
hence (U -deltaInterpreter) " {1} = { <*u,u*> where u is Element of U : verum } ; :: thesis: verum