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 set ; :: 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 A3: ( e is finite Subset of t & ex x, y being set st
( x in t & y in t & not x = y & e = {x,y} ) ) by Th10;
consider x, y being set such that
A4: ( x in t & y in t & not x = y & e = {x,y} ) by A2, Th10;
e is finite Subset of u by A1, A3, XBOOLE_1:1;
hence e in TWOELEMENTSETS u by A1, A4, Th10; :: thesis: verum