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