definition
mode nlt2_elements -> set means
:DF2:
ex a,b st a
Cit & bCit & a <> b;existence
proof
take B = NAT
thus ex a,b st a
CB & bCB & a <> bproof
take a = 1, b = 2;
thus a
CB & bCB & a <> b;end;
end;
end;
definition
attr nlt2_elements -> set means :DF2:
ex a,b st a
Cit & bCit & a<>b;end;
definition
cluster nlt2_elements set;
existence
proof
take B=NAT;
ex a,b st a
CB & bCB & a<>bproof
take a=1 , b=2;
thus a
CB & bCB & a<>b;end;
hence thesis by DF2;
end;
end;
A is non_empty
Or, the adjective form.
non-empty set
In this case, non-empty is the same with non empty.
definition
attr empty -> set means :A1:
not ex x st x
Cit;...
synonym (symbol);
antonym (symbol);
end;
finite infinite set
empty non-empty set
Existence | Uniqueness | |
---|---|---|
Mode | ||
Pred | ||
Functor | ||
Attr |