<*0, the Element of NAT *> in VAR ;
hence not VAR is empty ; :: thesis: VAR is antichain-like
for p being FinSequence st p in VAR holds
dom p = {1,2}

proof

let p be FinSequence; :: thesis: ( p in VAR implies dom p = {1,2} )
assume p in VAR ; :: thesis: dom p = {1,2}
then consider k being Element of NAT such that
A2: p = <*0,k*> ;
thus dom p = {1,2} by A2, FINSEQ_1:92; :: thesis: verum

end;

hence VAR is antichain-like by POLNOT_1:45; :: thesis: verum