reconsider f = Y --> TRUE as Function of Y,BOOLEAN ;
reconsider f = f as Function of Y,BOOLEAN ;
take f ; :: thesis: for x being Element of Y holds f . x = TRUE
let x be Element of Y; :: thesis: f . x = TRUE
thus f . x = TRUE ; :: thesis: verum