let k be Element of NAT ; :: thesis: for a being non empty Element of (SubstPoset (NAT,{k})) st a <> {{}} holds
ex f being finite Function st
( f in a & f <> {} )
let a be non empty Element of (SubstPoset (NAT,{k})); :: thesis: ( a <> {{}} implies ex f being finite Function st
( f in a & f <> {} ) )
assume A1: a <> {{}} ; :: thesis: ex f being finite Function st
( f in a & f <> {} )
consider f being object such that
A2: f in a by XBOOLE_0:def 1;
SubstitutionSet (NAT,{k}) = the carrier of (SubstPoset (NAT,{k})) by SUBSTLAT:def 4;
then reconsider f = f as finite Function by A2, HEYTING2:1;
take f ; :: thesis: ( f in a & f <> {} )
thus f in a by A2; :: thesis: f <> {}
assume f = {} ; :: thesis: contradiction
hence contradiction by A1, A2, Th32; :: thesis: verum