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

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

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

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

end;

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

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

end;

end;