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