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

( (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