let A, B be set ; :: thesis: for x being object st x in B holds

(A --> x) " B = A

let x be object ; :: thesis: ( x in B implies (A --> x) " B = A )

assume A1: x in B ; :: thesis: (A --> x) " B = A

hence (A --> x) " B = A ; :: thesis: verum

(A --> x) " B = A

let x be object ; :: thesis: ( x in B implies (A --> x) " B = A )

assume A1: x in B ; :: thesis: (A --> x) " B = A

hence (A --> x) " B = A ; :: thesis: verum