theorem :: GLIBPRE0:6

for X being set
for Y being non empty set holds
( X c< Y iff X is proper Subset of Y ) by SUBSET_1:def 6, XBOOLE_0:def 8;