let x be Element of (InclPoset (Filt L)); :: thesis: not x is empty
InclPoset (Filt L) = RelStr(# (Filt L),(RelIncl (Filt L)) #) by YELLOW_1:def 1;
then x in Filt L ;
then ex X being Filter of L st x = X ;
hence not x is empty ; :: thesis: verum