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 consider X being Filter of L such that
A1: x = X ;
thus not x is empty by A1; :: thesis: verum