let F1, F2 be set ; :: thesis: ( ( for x being set holds
( x in F1 iff x is RoughSet of X ) ) & ( for x being set holds
( x in F2 iff x is RoughSet of X ) ) implies F1 = F2 )
assume A3: ( ( for x being set holds
( x in F1 iff x is RoughSet of X ) ) & ( for x being set holds
( x in F2 iff x is RoughSet of X ) ) ) ; :: thesis: F1 = F2

now

let x be set ; :: thesis: ( x in F1 iff x in F2 )
( ( x in F1 implies x is RoughSet of X ) & ( x is RoughSet of X implies x in F1 ) & ( x in F2 implies x is RoughSet of X ) & ( x is RoughSet of X implies x in F2 ) ) by A3;
hence ( x in F1 iff x in F2 ) ; :: thesis: verum

end;

hence F1 = F2 by TARSKI:2; :: thesis: verum