let A be Formula of L; AOFA_L00:def 42 for B, C being Formula of L holds
( A \imp (B \imp A) in [#] ( the Sorts of L . the formula-sort of S) & (A \imp (B \imp C)) \imp ((A \imp B) \imp (A \imp C)) in [#] ( the Sorts of L . the formula-sort of S) & ((\not A) \imp (\not B)) \imp (B \imp A) in [#] ( the Sorts of L . the formula-sort of S) & A \imp (A \or B) in [#] ( the Sorts of L . the formula-sort of S) & A \imp (B \or A) in [#] ( the Sorts of L . the formula-sort of S) & (A \imp C) \imp ((B \imp C) \imp ((A \or B) \imp C)) in [#] ( the Sorts of L . the formula-sort of S) & (A \and B) \imp A in [#] ( the Sorts of L . the formula-sort of S) & (A \and B) \imp B in [#] ( the Sorts of L . the formula-sort of S) & A \imp (B \imp (A \and B)) in [#] ( the Sorts of L . the formula-sort of S) & (A \and (\not A)) \imp B in [#] ( the Sorts of L . the formula-sort of S) & (A \imp B) \imp ((A \imp (\not B)) \imp (\not A)) in [#] ( the Sorts of L . the formula-sort of S) & A \or (\not A) in [#] ( the Sorts of L . the formula-sort of S) & (A \iff B) \imp (A \imp B) in [#] ( the Sorts of L . the formula-sort of S) & (A \iff B) \imp (B \imp A) in [#] ( the Sorts of L . the formula-sort of S) & ((A \imp B) \and (B \imp A)) \imp (A \iff B) in [#] ( the Sorts of L . the formula-sort of S) & \true_ L in [#] ( the Sorts of L . the formula-sort of S) & ((\true_ L) \and A) \iff A in [#] ( the Sorts of L . the formula-sort of S) & ((\true_ L) \or A) \iff (\true_ L) in [#] ( the Sorts of L . the formula-sort of S) & ( A in [#] ( the Sorts of L . the formula-sort of S) & A \imp B in [#] ( the Sorts of L . the formula-sort of S) implies B in [#] ( the Sorts of L . the formula-sort of S) ) )
( [#] ( the Sorts of L . the formula-sort of S) = the Sorts of L . the formula-sort of S & not the Sorts of L . the formula-sort of S is empty )
by Def18, SUBSET_1:def 3;
hence
for B, C being Formula of L holds
( A \imp (B \imp A) in [#] ( the Sorts of L . the formula-sort of S) & (A \imp (B \imp C)) \imp ((A \imp B) \imp (A \imp C)) in [#] ( the Sorts of L . the formula-sort of S) & ((\not A) \imp (\not B)) \imp (B \imp A) in [#] ( the Sorts of L . the formula-sort of S) & A \imp (A \or B) in [#] ( the Sorts of L . the formula-sort of S) & A \imp (B \or A) in [#] ( the Sorts of L . the formula-sort of S) & (A \imp C) \imp ((B \imp C) \imp ((A \or B) \imp C)) in [#] ( the Sorts of L . the formula-sort of S) & (A \and B) \imp A in [#] ( the Sorts of L . the formula-sort of S) & (A \and B) \imp B in [#] ( the Sorts of L . the formula-sort of S) & A \imp (B \imp (A \and B)) in [#] ( the Sorts of L . the formula-sort of S) & (A \and (\not A)) \imp B in [#] ( the Sorts of L . the formula-sort of S) & (A \imp B) \imp ((A \imp (\not B)) \imp (\not A)) in [#] ( the Sorts of L . the formula-sort of S) & A \or (\not A) in [#] ( the Sorts of L . the formula-sort of S) & (A \iff B) \imp (A \imp B) in [#] ( the Sorts of L . the formula-sort of S) & (A \iff B) \imp (B \imp A) in [#] ( the Sorts of L . the formula-sort of S) & ((A \imp B) \and (B \imp A)) \imp (A \iff B) in [#] ( the Sorts of L . the formula-sort of S) & \true_ L in [#] ( the Sorts of L . the formula-sort of S) & ((\true_ L) \and A) \iff A in [#] ( the Sorts of L . the formula-sort of S) & ((\true_ L) \or A) \iff (\true_ L) in [#] ( the Sorts of L . the formula-sort of S) & ( A in [#] ( the Sorts of L . the formula-sort of S) & A \imp B in [#] ( the Sorts of L . the formula-sort of S) implies B in [#] ( the Sorts of L . the formula-sort of S) ) )
; verum