set M = NAT --> {};

A1: now :: thesis: for x being object st x in NAT holds
(NAT --> {}) . x in bool props

let x be object ; :: thesis: ( x in NAT implies (NAT --> {}) . x in bool props )
assume x in NAT ; :: thesis: (NAT --> {}) . x in bool props
then A2: (NAT --> {}) . x = {} by FUNCOP_1:7;
{} c= props ;
hence (NAT --> {}) . x in bool props by A2; :: thesis: verum

end;

dom (NAT --> {}) = NAT by FUNCOP_1:13;
hence NAT --> {} is LTLModel by A1, FUNCT_2:3; :: thesis: verum