now

let x be set ; :: thesis: ( x in {[1,1,1]} implies x in [:{1},{1},{1}:] )
assume x in {[1,1,1]} ; :: thesis: x in [:{1},{1},{1}:]
then x = [1,1,1] by TARSKI:def 1;
hence x in [:{1},{1},{1}:] by Lm1, MCART_1:73; :: thesis: verum

end;

hence {[1,1,1]} c= [:{1},{1},{1}:] by TARSKI:def 3; :: thesis: verum