let A be MP-wff; :: thesis: ( 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 )

now :: thesis: ( 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 )

per cases ( card (dom A) = 1 or card (dom A) > 1 ) by NAT_1:25;

suppose card (dom A) = 1 ; :: thesis: ( 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 )

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: verum

end;

suppose card (dom A) > 1 ; :: thesis: ( 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 )

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: verum

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: verum