let x1, x2, Z be set ; :: thesis: ( {x1,x2} c= Z iff ( x1 in Z & x2 in Z ) )
( x1 in {x1,x2} & x2 in {x1,x2} ) by TARSKI:def 2;
hence ( {x1,x2} c= Z implies ( x1 in Z & x2 in Z ) ) by TARSKI:def 3; :: thesis: ( x1 in Z & x2 in Z implies {x1,x2} c= Z )
assume A1: ( x1 in Z & x2 in Z ) ; :: thesis: {x1,x2} c= Z
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in {x1,x2} or z in Z )
assume z in {x1,x2} ; :: thesis: z in Z
hence z in Z by A1, TARSKI:def 2; :: thesis: verum