let X be set ; :: thesis: for T being Tolerance of X holds union (TolSets T) = X
let T be Tolerance of X; :: thesis: union (TolSets T) = X
for x being set holds
( x in union (TolSets T) iff x in X )

proof

let x be set ; :: thesis: ( x in union (TolSets T) iff x in X )
thus ( x in union (TolSets T) implies x in X ) :: thesis: ( x in X implies x in union (TolSets T) )

proof

assume x in union (TolSets T) ; :: thesis: x in X
then consider Z being set such that
A1: ( x in Z & Z in TolSets T ) by TARSKI:def 4;
Z is TolSet of T by A1, Def6;
then Z c= X by Th43;
hence x in X by A1; :: thesis: verum

end;

assume x in X ; :: thesis: x in union (TolSets T)
then consider Z being TolClass of T such that
A2: x in Z by Th47;
Z in TolSets T by Def6;
hence x in union (TolSets T) by A2, TARSKI:def 4; :: thesis: verum

end;

hence union (TolSets T) = X by TARSKI:2; :: thesis: verum