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;

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 )
;

end;

suppose A1:
s is relational
; :: thesis: ex b_{1} being Interpreter of s,U st b_{1} 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_{1} being Interpreter of s,U st b_{1} is E -respecting
; :: thesis: verum

end;gg is E -respecting by Def10, A1;

hence ex b

suppose A2:
not s is relational
; :: thesis: ex b_{1} being Interpreter of s,U st b_{1} 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_{1} being Interpreter of s,U st b_{1} is E -respecting
; :: thesis: verum

end;ff is E -respecting by Def10, A2;

hence ex b