let v1 be Element of VAR ; :: thesis: code {v1} = {(x". v1)}
thus code {v1} c= {(x". v1)} :: according to XBOOLE_0:def 10 :: thesis: {(x". v1)} c= code {v1}
proof
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in code {v1} or p in {(x". v1)} )
assume p in code {v1} ; :: thesis: p in {(x". v1)}
then consider v2 being Element of VAR such that
A1: v2 in {v1} and
A2: p = x". v2 by Lm5;
v2 = v1 by A1, TARSKI:def 1;
hence p in {(x". v1)} by A2, TARSKI:def 1; :: thesis: verum
end;
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in {(x". v1)} or p in code {v1} )
assume p in {(x". v1)} ; :: thesis: p in code {v1}
then A3: p = x". v1 by TARSKI:def 1;
v1 in {v1} by TARSKI:def 1;
hence p in code {v1} by A3, Lm5; :: thesis: verum