let UN be Universe; :: thesis: for A, B being non empty set st [:A,B:] is Element of UN holds
( A is Element of UN & B is Element of UN )
let A, B be non empty set ; :: thesis: ( [:A,B:] is Element of UN implies ( A is Element of UN & B is Element of UN ) )
assume A1: [:A,B:] is Element of UN ; :: thesis: ( A is Element of UN & B is Element of UN )
( proj1 [:A,B:] = A & proj2 [:A,B:] = B ) by FUNCT_5:9;
hence ( A is Element of UN & B is Element of UN ) by A1, Th36; :: thesis: verum