let D1, D2 be set ; :: thesis: ( ( for x being set holds
( x in D1 iff x is Chain of f ) ) & ( for x being set holds
( x in D2 iff x is Chain of f ) ) implies D1 = D2 )
assume A2: for x being set holds
( x in D1 iff x is Chain of f ) ; :: thesis: ( ex x being set st
( ( x in D2 implies x is Chain of f ) implies ( x is Chain of f & not x in D2 ) ) or D1 = D2 )
assume A3: for x being set holds
( x in D2 iff x is Chain of f ) ; :: thesis: D1 = D2
thus D1 c= D2 :: according to XBOOLE_0:def 10 :: thesis: D2 c= D1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in D1 or x in D2 )
assume x in D1 ; :: thesis: x in D2
then x is Chain of f by A2;
hence x in D2 by A3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in D2 or x in D1 )
assume x in D2 ; :: thesis: x in D1
then x is Chain of f by A3;
hence x in D1 by A2; :: thesis: verum