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

( <*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