let L be non empty RelStr ; :: thesis: for x, y being Element of L holds

( y in uparrow x iff x <= y )

let x, y be Element of L; :: thesis: ( y in uparrow x iff x <= y )

A1: uparrow x = { z where z is Element of L : ex v being Element of L st

( z >= v & v in {x} ) } by Th15;

then ( y in uparrow x iff ex z being Element of L st

( y = z & ex v being Element of L st

( z >= v & v in {x} ) ) ) ;

hence ( y in uparrow x implies y >= x ) by TARSKI:def 1; :: thesis: ( x <= y implies y in uparrow x )

x in {x} by TARSKI:def 1;

hence ( x <= y implies y in uparrow x ) by A1; :: thesis: verum

( y in uparrow x iff x <= y )

let x, y be Element of L; :: thesis: ( y in uparrow x iff x <= y )

A1: uparrow x = { z where z is Element of L : ex v being Element of L st

( z >= v & v in {x} ) } by Th15;

then ( y in uparrow x iff ex z being Element of L st

( y = z & ex v being Element of L st

( z >= v & v in {x} ) ) ) ;

hence ( y in uparrow x implies y >= x ) by TARSKI:def 1; :: thesis: ( x <= y implies y in uparrow x )

x in {x} by TARSKI:def 1;

hence ( x <= y implies y in uparrow x ) by A1; :: thesis: verum