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

( y in downarrow x iff y <= x )

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

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

( z <= v & v in {x} ) } by Th14;

then ( y in downarrow 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 downarrow x implies y <= x ) by TARSKI:def 1; :: thesis: ( y <= x implies y in downarrow x )

x in {x} by TARSKI:def 1;

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

( y in downarrow x iff y <= x )

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

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

( z <= v & v in {x} ) } by Th14;

then ( y in downarrow 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 downarrow x implies y <= x ) by TARSKI:def 1; :: thesis: ( y <= x implies y in downarrow x )

x in {x} by TARSKI:def 1;

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