:: deftheorem defines PLO2bis CARDFIL2:def 19 :
for X being set
for x being Subset of X holds PLO2bis x = x;