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