theorem :: FINSEQ_6:52

for D being non empty set
for p being Element of D holds
( <*p*> :- p = <*p*> & <*p*> -: p = <*p*> )