let z be set ; :: thesis: ( <*z*> |-- z = {} & <*z*> -| z = {} )
z in {z} by TARSKI:def 1;
then A1: z in rng <*z*> by FINSEQ_1:39;
A2: z .. <*z*> = 1 by Th18;
len <*z*> = 1 by FINSEQ_1:39;
hence <*z*> |-- z = {} by A1, A2, FINSEQ_4:49; :: thesis: <*z*> -| z = {}
thus <*z*> -| z = {} by A1, A2, FINSEQ_4:40; :: thesis: verum