let L be non empty RelStr ; :: thesis: for p, x being Element of L holds
( (chi ((downarrow p) ` ),the carrier of L) . x = {} iff x <= p )
let p, x be Element of L; :: thesis: ( (chi ((downarrow p) ` ),the carrier of L) . x = {} iff x <= p )
( not x in (downarrow p) ` iff x in downarrow p ) by XBOOLE_0:def 5;
hence ( (chi ((downarrow p) ` ),the carrier of L) . x = {} iff x <= p ) by FUNCT_3:def 3, WAYBEL_0:17; :: thesis: verum