let t, u be set ; :: thesis: ( t c= u implies TWOELEMENTSETS t c= TWOELEMENTSETS u )
assume A1: t c= u ; :: thesis: TWOELEMENTSETS t c= TWOELEMENTSETS u
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in TWOELEMENTSETS t or e in TWOELEMENTSETS u )
assume A2: e in TWOELEMENTSETS t ; :: thesis: e in TWOELEMENTSETS u
then e is finite Subset of t by Th8;
then A3: e is finite Subset of u by A1, XBOOLE_1:1;
ex x, y being object st
( x in t & y in t & not x = y & e = {x,y} ) by A2, Th8;
hence e in TWOELEMENTSETS u by A1, A3, Th8; :: thesis: verum