take pr1 (S, the carrier of A) ; :: thesis: ( pr1 (S, the carrier of A) is complying_with_empty-instruction & pr1 (S, the carrier of A) is complying_with_catenation & pr1 (S, the carrier of A) complies_with_if_wrt T & pr1 (S, the carrier of A) complies_with_while_wrt T )
thus ( pr1 (S, the carrier of A) is complying_with_empty-instruction & pr1 (S, the carrier of A) is complying_with_catenation & pr1 (S, the carrier of A) complies_with_if_wrt T & pr1 (S, the carrier of A) complies_with_while_wrt T ) by Th81; :: thesis: verum