:: deftheorem defines all-square-uparrow CARDFIL4:def 6 :
all-square-uparrow = { (square-uparrow n) where n is Nat : verum } ;