let m be Element of NAT ; :: thesis: for a being Element of (SubstPoset NAT ,{m}) st PFDrt m is_>=_than a holds
a <> {{} }
reconsider P1 = PFBrt 1,m as Element of (SubstPoset NAT ,{m}) by Th28;
let a be Element of (SubstPoset NAT ,{m}); :: thesis: ( PFDrt m is_>=_than a implies a <> {{} } )
assume A1: PFDrt m is_>=_than a ; :: thesis: a <> {{} }
PFBrt 1,m in PFDrt m by Def5;
then A2: P1 >= a by A1, LATTICE3:def 8;
assume A3: a = {{} } ; :: thesis: contradiction
Top (SubstPoset NAT ,{m}) = {{} } by Th39;
hence contradiction by A3, A2, Th30, WAYBEL15:5; :: thesis: verum