let v1, v2 be Element of VAR ; :: thesis: code {v1,v2} = {(x". v1),(x". v2)}
thus code {v1,v2} c= {(x". v1),(x". v2)} :: according to XBOOLE_0:def 10 :: thesis: {(x". v1),(x". v2)} c= code {v1,v2}

proof

let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in code {v1,v2} or p in {(x". v1),(x". v2)} )
assume p in code {v1,v2} ; :: thesis: p in {(x". v1),(x". v2)}
then ex v3 being Element of VAR st
( v3 in {v1,v2} & p = x". v3 ) by Lm5;
then ( p = x". v1 or p = x". v2 ) by TARSKI:def 2;
hence p in {(x". v1),(x". v2)} by TARSKI:def 2; :: thesis: verum

end;

let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in {(x". v1),(x". v2)} or p in code {v1,v2} )
assume A1: p in {(x". v1),(x". v2)} ; :: thesis: p in code {v1,v2}

now :: thesis: p in code {v1,v2}

per cases ( p = x". v1 or p = x". v2 ) by A1, TARSKI:def 2;

suppose A2: p = x". v1 ; :: thesis: p in code {v1,v2}

v1 in {v1,v2} by TARSKI:def 2;
hence p in code {v1,v2} by A2, Lm5; :: thesis: verum

end;

suppose A3: p = x". v2 ; :: thesis: p in code {v1,v2}

v2 in {v1,v2} by TARSKI:def 2;
hence p in code {v1,v2} by A3, Lm5; :: thesis: verum

end;

end;

end;

hence p in code {v1,v2} ; :: thesis: verum