let X be set ; 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 ; ( [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):]
; ( not c in X or not [a,b] = [c,{c}] or ( a = c & b = {c} ) )
assume
c in X
; ( not [a,b] = [c,{c}] or ( a = c & b = {c} ) )
assume A1:
[a,b] = [c,{c}]
; ( 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; verum