reconsider x9 = 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 that

A3: z in uparrow x and

A4: y in uparrow x ; :: thesis: ex z being Element of L st

( z in uparrow x & z <= z & z <= y )

take x9 ; :: thesis: ( x9 in uparrow x & x9 <= z & x9 <= y )

x9 <= x9 ;

hence ( x9 in uparrow x & x9 <= z & x9 <= y ) by A3, A4, Th18; :: thesis: verum

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 that

A3: z in uparrow x and

A4: y in uparrow x ; :: thesis: ex z being Element of L st

( z in uparrow x & z <= z & z <= y )

take x9 ; :: thesis: ( x9 in uparrow x & x9 <= z & x9 <= y )

x9 <= x9 ;

hence ( x9 in uparrow x & x9 <= z & x9 <= y ) by A3, A4, Th18; :: thesis: verum