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