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