set O = OwnSymbolsOf S;
defpred S1[ object , object ] means ex s being own Element of S st
( \$1 = s & \$2 is Interpreter of s,U );
A1: for x being object st x in OwnSymbolsOf S holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in OwnSymbolsOf S implies ex y being object st S1[x,y] )
assume x in OwnSymbolsOf S ; :: thesis: ex y being object st S1[x,y]
then reconsider s = x as own Element of S by FOMODEL1:def 19;
take y = the Interpreter of s,U; :: thesis: S1[x,y]
take s ; :: thesis: ( x = s & y is Interpreter of s,U )
thus ( x = s & y is Interpreter of s,U ) ; :: thesis: verum
end;
consider f being Function such that
A2: ( dom f = OwnSymbolsOf S & ( for s being object st s in OwnSymbolsOf S holds
S1[s,f . s] ) ) from take f ; :: thesis: for s being own Element of S holds f . s is Interpreter of s,U
thus for s being own Element of S holds f . s is Interpreter of s,U :: thesis: verum
proof
let s be own Element of S; :: thesis: f . s is Interpreter of s,U
consider s1 being own Element of S such that
A3: ( s = s1 & f . s is Interpreter of s1,U ) by ;
thus f . s is Interpreter of s,U by A3; :: thesis: verum
end;