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

proof

let x be object ; :: thesis: ( x in union (TolClasses T) iff x in X )
thus ( x in union (TolClasses T) implies x in X ) :: thesis: ( x in X implies x in union (TolClasses T) )

proof

assume x in union (TolClasses T) ; :: thesis: x in X
then consider Z being set such that
A1: x in Z and
A2: Z in TolClasses T by TARSKI:def 4;
Z is TolSet of T by A2, Def4;
then Z c= X by Th18;
hence x in X by A1; :: thesis: verum

end;

assume x in X ; :: thesis: x in union (TolClasses T)
then consider Z being TolClass of T such that
A3: x in Z by Th21;
Z in TolClasses T by Def4;
hence x in union (TolClasses T) by A3, TARSKI:def 4; :: thesis: verum

end;

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