let x, X be set ; :: thesis: ( x in Toler_on_subsets X iff ex A being set st
( A c= X & x is Tolerance of A ) )
set f = { (Toler Y) where Y is Subset of X : verum } ;
thus ( x in Toler_on_subsets X implies ex A being set st
( A c= X & x is Tolerance of A ) ) :: thesis: ( ex A being set st
( A c= X & x is Tolerance of A ) implies x in Toler_on_subsets X )

proof

assume x in Toler_on_subsets X ; :: thesis: ex A being set st
( A c= X & x is Tolerance of A )
then consider a being set such that
A1: x in a and
A2: a in { (Toler Y) where Y is Subset of X : verum } by TARSKI:def 4;
consider Y being Subset of X such that
A3: a = Toler Y by A2;
take Y ; :: thesis: ( Y c= X & x is Tolerance of Y )
thus ( Y c= X & x is Tolerance of Y ) by A1, A3, Def15; :: thesis: verum

end;

given A being set such that A4: A c= X and
A5: x is Tolerance of A ; :: thesis: x in Toler_on_subsets X
reconsider A = A as Subset of X by A4;
A6: Toler A in { (Toler Y) where Y is Subset of X : verum } ;
x in Toler A by A5, Def15;
hence x in Toler_on_subsets X by A6, TARSKI:def 4; :: thesis: verum