theorem :: ZF_LANG1:110

for p being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= p => (p '&' p) & M |= p => (p '&' p) )