set UN = FinSETS ;
take FinSETS ; :: thesis: FinSETS is trivial
thus FinSETS is trivial by Th19, Th20; :: thesis: verum