theorem :: SUBSET_1:34

for X being set
for x1, x2 being Element of X st X <> {} holds
{x1,x2} is Subset of X