let k be Element of NAT ; :: thesis: PFBrt (1,k) <> {{}}
PFArt (1,k) in PFBrt (1,k) by Def4;
hence PFBrt (1,k) <> {{}} by TARSKI:def 1; :: thesis: verum