set p = [(<*> LTLB_WFF),(<*> LTLB_WFF)];
take [(<*> LTLB_WFF),(<*> LTLB_WFF)] ; :: thesis: ( [(<*> LTLB_WFF),(<*> LTLB_WFF)] is consistent & [(<*> LTLB_WFF),(<*> LTLB_WFF)] is complete )
thus ( [(<*> LTLB_WFF),(<*> LTLB_WFF)] is consistent & [(<*> LTLB_WFF),(<*> LTLB_WFF)] is complete ) ; :: thesis: verum