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 & a in { (Toler Y) where Y is Subset of X : verum } ) by TARSKI:def 4;
consider Y being Subset of X such that
A2: a = Toler Y by A1;
take Y ; :: thesis: ( Y c= X & x is Tolerance of Y )
thus ( Y c= X & x is Tolerance of Y ) by A1, A2, Def19; :: thesis: verum

end;

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