set M = NAT --> {};

hence NAT --> {} is LTLModel by A1, FUNCT_2:3; :: thesis: verum

A1: now :: thesis: for x being object st x in NAT holds

(NAT --> {}) . x in bool props

dom (NAT --> {}) = NAT
by FUNCOP_1:13;(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;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

hence NAT --> {} is LTLModel by A1, FUNCT_2:3; :: thesis: verum