reconsider x' = x as Element of L ;
thus not uparrow x is empty ; :: thesis: uparrow x is filtered
let z, y be Element of L; :: according to WAYBEL_0:def 2 :: thesis: ( z in uparrow x & y in uparrow x implies ex z being Element of L st
( z in uparrow x & z <= z & z <= y ) )
assume A2: ( z in uparrow x & y in uparrow x ) ; :: thesis: ex z being Element of L st
( z in uparrow x & z <= z & z <= y )
take x' ; :: thesis: ( x' in uparrow x & x' <= z & x' <= y )
x' <= x' ;
hence ( x' in uparrow x & x' <= z & x' <= y ) by A2, Th18; :: thesis: verum