theorem(![A,B,C]:(subset(A,B) & subset(B,C) => subset(A,C))).
definition(subset(A,B) <=> ! [X]:member(X,A) => member(X,B)).