let X be set ; :: thesis: for a, b, c being object st [a,b] in [:X,(bool X):] & c in X & [a,b] = [c,{c}] holds
( a = c & b = {c} )
let a, b, c be object ; :: thesis: ( [a,b] in [:X,(bool X):] & c in X & [a,b] = [c,{c}] implies ( a = c & b = {c} ) )
assume [a,b] in [:X,(bool X):] ; :: thesis: ( not c in X or not [a,b] = [c,{c}] or ( a = c & b = {c} ) )
assume c in X ; :: thesis: ( not [a,b] = [c,{c}] or ( a = c & b = {c} ) )
assume A1: [a,b] = [c,{c}] ; :: thesis: ( a = c & b = {c} )
( [a,b] `1 = a & [a,b] `2 = b & [c,{c}] `1 = c & [c,{c}] `2 = {c} ) ;
hence ( a = c & b = {c} ) by A1; :: thesis: verum