take Lukasiewicz_implication ; :: thesis: Lukasiewicz_implication is with_properties_of_fuzzy_implication
thus Lukasiewicz_implication is with_properties_of_fuzzy_implication ; :: thesis: verum