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:39;
hence <*p*> :- p = <*p*> ^ (<*p*> |-- p) by Th41
.= <*p*> ^ {} by Th32
.= <*p*> by FINSEQ_1:34 ;
:: thesis: <*p*> -: p = <*p*>
thus <*p*> -: p = (<*p*> -| p) ^ <*p*> by A1, Th40
.= {} ^ <*p*> by Th32
.= <*p*> by FINSEQ_1:34 ; :: thesis: verum