theorem :: LFUZZY_1:20

for X being non empty set
for R, R9 being RMembership_Func of X,X st R9 is symmetric & R9 c= holds
R9 c=