set n = abs (ar s);
reconsider EE = (abs (ar s)) -placesOf E as Equivalence_Relation of ((abs (ar s)) -tuples_on U) ;
set f = the (abs (ar s)) -placesOf E,E -respecting Function of ((abs (ar s)) -tuples_on U),U;
set g = the (abs (ar s)) -placesOf E, id BOOLEAN -respecting Function of ((abs (ar s)) -tuples_on U),BOOLEAN;

per cases ( s is relational or not s is relational ) ;

suppose C1: s is relational ; :: thesis: ex b₁ being Interpreter of s,U st b₁ is E -respecting

then reconsider gg = the (abs (ar s)) -placesOf E, id BOOLEAN -respecting Function of ((abs (ar s)) -tuples_on U),BOOLEAN as Interpreter of s,U by FOMODEL2:def 2;
gg is E -respecting by DefCompatible2, C1;
hence ex b₁ being Interpreter of s,U st b₁ is E -respecting ; :: thesis: verum

end;

suppose C1: not s is relational ; :: thesis: ex b₁ being Interpreter of s,U st b₁ is E -respecting

then reconsider ff = the (abs (ar s)) -placesOf E,E -respecting Function of ((abs (ar s)) -tuples_on U),U as Interpreter of s,U by FOMODEL2:def 2;
ff is E -respecting by DefCompatible2, C1;
hence ex b₁ being Interpreter of s,U st b₁ is E -respecting ; :: thesis: verum

end;

end;