let R be non empty RelStr ; :: thesis: for x, y being Element of R holds
( y in (uparrow x) ` iff not x <= y )
let x, y be Element of R; :: thesis: ( y in (uparrow x) ` iff not x <= y )
(uparrow x) ` = the carrier of R \ (uparrow x) by SUBSET_1:def 4;
then ( y in (uparrow x) ` iff not y in uparrow x ) by XBOOLE_0:def 5;
hence ( y in (uparrow x) ` iff not x <= y ) by WAYBEL_0:18; :: thesis: verum