let u, v, x, y be set ; :: thesis: ( <%u,v%> = <%x,y%> implies ( u = x & v = y ) )
( <%u,v%> . 0 = u & <%u,v%> . 1 = v & <%x,y%> . 0 = x & <%x,y%> . 1 = y ) ;
hence ( <%u,v%> = <%x,y%> implies ( u = x & v = y ) ) ; :: thesis: verum