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