let A, x be set ; :: thesis: (A --> x) " {x} = A
x in {x} by TARSKI:def 1;
hence (A --> x) " {x} = A by Th20; :: thesis: verum