let X be non empty set ; :: thesis: for x, y, z being Element of X st x in (singleton X) . z & y in (singleton X) . z holds
x = y
let x, y, z be Element of X; :: thesis: ( x in (singleton X) . z & y in (singleton X) . z implies x = y )
assume that
A1: x in (singleton X) . z and
A2: y in (singleton X) . z ; :: thesis: x = y
x = z by A1, Th52;
hence x = y by A2, Th52; :: thesis: verum