let x1, x2 be object ; :: thesis: for Z being set holds
( {x1,x2} c= Z iff ( x1 in Z & x2 in Z ) )
let 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 ) ) ; :: 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 object ; :: 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