let A be MP-wff; :: thesis:

now :: thesis:

per cases by NAT_1:25;

suppose card (dom A) = 1 ; :: thesis:

hence ( A = VERUM or ex p being MP-variable st A = @ p or ex B being MP-wff st A = 'not' B or ex B being MP-wff st A = (#) B or ex B, C being MP-wff st A = B '&' C ) by Th31; :: thesis:

end;

suppose card (dom A) > 1 ; :: thesis:

then card (dom A) >= 1 + 1 by NAT_1:13;
hence ( A = VERUM or ex p being MP-variable st A = @ p or ex B being MP-wff st A = 'not' B or ex B being MP-wff st A = (#) B or ex B, C being MP-wff st A = B '&' C ) by Th32; :: thesis:

end;

end;

end;

hence ( A = VERUM or ex p being MP-variable st A = @ p or ex B being MP-wff st A = 'not' B or ex B being MP-wff st A = (#) B or ex B, C being MP-wff st A = B '&' C ) ; :: thesis: