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 Th25;
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;
assume A3: a = {{}} ; :: thesis: contradiction
Top (SubstPoset (NAT,{m})) = {{}} by Th36;
hence contradiction by A3, A2, Th27, WAYBEL15:3; :: thesis: verum