set p = n |-> {{}};

take n |-> {{}} ; :: thesis: n |-> {{}} is non-empty

not {} in rng (n |-> {{}})

take n |-> {{}} ; :: thesis: n |-> {{}} is non-empty

not {} in rng (n |-> {{}})

proof

hence
n |-> {{}} is non-empty
by RELAT_1:def 9; :: thesis: verum
assume
{} in rng (n |-> {{}})
; :: thesis: contradiction

then consider a being object such that

A1: a in dom (n |-> {{}}) and

A2: {} = (n |-> {{}}) . a by FUNCT_1:def 3;

a in Seg n by FINSEQ_1:89, A1;

hence contradiction by A2, FINSEQ_2:57; :: thesis: verum

end;then consider a being object such that

A1: a in dom (n |-> {{}}) and

A2: {} = (n |-> {{}}) . a by FUNCT_1:def 3;

a in Seg n by FINSEQ_1:89, A1;

hence contradiction by A2, FINSEQ_2:57; :: thesis: verum