let U be Universe; :: thesis: union { the carrier of (Trivial-addLoopStr x) where x is Element of U : verum } = U
set T = { the carrier of (Trivial-addLoopStr x) where x is Element of U : verum } ;

now :: thesis: ( ( for o being object st o in union { the carrier of (Trivial-addLoopStr x) where x is Element of U : verum } holds
o in U ) & union { the carrier of (Trivial-addLoopStr x) where x is Element of U : verum } c= U & ( for o being object st o in U holds
o in union { the carrier of (Trivial-addLoopStr x) where x is Element of U : verum } ) & U c= union { the carrier of (Trivial-addLoopStr x) where x is Element of U : verum } )

hereby :: thesis: ( union { the carrier of (Trivial-addLoopStr x) where x is Element of U : verum } c= U & ( for o being object st o in U holds
o in union { the carrier of (Trivial-addLoopStr x) where x is Element of U : verum } ) & U c= union { the carrier of (Trivial-addLoopStr x) where x is Element of U : verum } )

let o be object ; :: thesis: ( o in union { the carrier of (Trivial-addLoopStr x) where x is Element of U : verum } implies o in U )
assume o in union { the carrier of (Trivial-addLoopStr x) where x is Element of U : verum } ; :: thesis: o in U
then consider y being set such that
A1: o in y and
A2: y in { the carrier of (Trivial-addLoopStr x) where x is Element of U : verum } by TARSKI:def 4;
consider x being Element of U such that
A3: y = the carrier of (Trivial-addLoopStr x) by A2;
o = x by A3, A1, TARSKI:def 1;
hence o in U ; :: thesis: verum

end;

hence union { the carrier of (Trivial-addLoopStr x) where x is Element of U : verum } c= U ; :: thesis: ( ( for o being object st o in U holds
o in union { the carrier of (Trivial-addLoopStr x) where x is Element of U : verum } ) & U c= union { the carrier of (Trivial-addLoopStr x) where x is Element of U : verum } )

hereby :: thesis: U c= union { the carrier of (Trivial-addLoopStr x) where x is Element of U : verum }

let o be object ; :: thesis: ( o in U implies o in union { the carrier of (Trivial-addLoopStr x) where x is Element of U : verum } )
assume o in U ; :: thesis: o in union { the carrier of (Trivial-addLoopStr x) where x is Element of U : verum }
then reconsider x = o as Element of U ;
{x} is Element of U ;
then reconsider y = the carrier of (Trivial-addLoopStr x) as Element of U ;
( o in y & y in { the carrier of (Trivial-addLoopStr x) where x is Element of U : verum } ) ;
hence o in union { the carrier of (Trivial-addLoopStr x) where x is Element of U : verum } by TARSKI:def 4; :: thesis: verum

end;

hence U c= union { the carrier of (Trivial-addLoopStr x) where x is Element of U : verum } ; :: thesis: verum

end;

hence union { the carrier of (Trivial-addLoopStr x) where x is Element of U : verum } = U ; :: thesis: verum