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

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