consider x being Element of L;
take uparrow x ; :: thesis: ( not uparrow x is empty & uparrow x is upper & uparrow x is filtered )
thus ( not uparrow x is empty & uparrow x is upper & uparrow x is filtered ) ; :: thesis: verum