let D be non empty set ; :: thesis: for p being Element of D holds
( <*p*> :- p = <*p*> & <*p*> -: p = <*p*> )
let p be Element of D; :: thesis: ( <*p*> :- p = <*p*> & <*p*> -: p = <*p*> )
p in {p} by TARSKI:def 1;
then A1: p in rng <*p*> by FINSEQ_1:56;
hence <*p*> :- p = <*p*> ^ (<*p*> |-- p) by Th45
.= <*p*> ^ {} by Th36
.= <*p*> by FINSEQ_1:47 ;
:: thesis: <*p*> -: p = <*p*>
thus <*p*> -: p = (<*p*> -| p) ^ <*p*> by A1, Th44
.= {} ^ <*p*> by Th36
.= <*p*> by FINSEQ_1:47 ; :: thesis: verum