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 ( x in (singleton X) . z & y in (singleton X) . z ) ; :: thesis: x = y
then ( x = z & y = z ) by Th68;
hence x = y ; :: thesis: verum