let A be Element of the Sorts of L . the formula-sort of S; :: according to AOFA_L00:def 43 :: thesis: for B being Element of the Sorts of L . the formula-sort of S
for x being Element of Union X holds
( ( for a being SortSymbol of J holds
( ( for t being Element of Union the Sorts of L st x in (X extended_by ({}, the carrier of S)) . a & t in the Sorts of L . a holds
for y being Element of Union (X extended_by ({}, the carrier of S)) st x = y holds
(\for (x,A)) \imp (A / (y,t)) in [#] ( the Sorts of L . the formula-sort of S) ) & ( x in X . a & x nin (vf A) . a implies (\for (x,(A \imp B))) \imp (A \imp (\for (x,B))) in [#] ( the Sorts of L . the formula-sort of S) ) ) ) & (\not (\ex (x,A))) \iff (\for (x,(\not A))) in [#] ( the Sorts of L . the formula-sort of S) & (\ex (x,(\not A))) \iff (\not (\for (x,A))) in [#] ( the Sorts of L . the formula-sort of S) & ( A in [#] ( the Sorts of L . the formula-sort of S) implies \for (x,A) 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 by SUBSET_1:def 3;
hence for B being Element of the Sorts of L . the formula-sort of S
for x being Element of Union X holds
( ( for a being SortSymbol of J holds
( ( for t being Element of Union the Sorts of L st x in (X extended_by ({}, the carrier of S)) . a & t in the Sorts of L . a holds
for y being Element of Union (X extended_by ({}, the carrier of S)) st x = y holds
(\for (x,A)) \imp (A / (y,t)) in [#] ( the Sorts of L . the formula-sort of S) ) & ( x in X . a & x nin (vf A) . a implies (\for (x,(A \imp B))) \imp (A \imp (\for (x,B))) in [#] ( the Sorts of L . the formula-sort of S) ) ) ) & (\not (\ex (x,A))) \iff (\for (x,(\not A))) in [#] ( the Sorts of L . the formula-sort of S) & (\ex (x,(\not A))) \iff (\not (\for (x,A))) in [#] ( the Sorts of L . the formula-sort of S) & ( A in [#] ( the Sorts of L . the formula-sort of S) implies \for (x,A) in [#] ( the Sorts of L . the formula-sort of S) ) ) ; :: thesis: verum