let UN be Universe; :: thesis: for X being Element of UN holds
( proj1 X is Element of UN & proj2 X is Element of UN )
let X be Element of UN; :: thesis: ( proj1 X is Element of UN & proj2 X is Element of UN )
( proj1 X in bool (union (union X)) & proj2 X in bool (union (union X)) & UN is axiom_GU1 ) by Th1;
hence ( proj1 X is Element of UN & proj2 X is Element of UN ) ; :: thesis: verum