let L be non empty reflexive RelStr ; :: thesis: for x, y being Element of L holds
( y in compactbelow x iff ( x >= y & y is compact ) )
let x, y be Element of L; :: thesis: ( y in compactbelow x iff ( x >= y & y is compact ) )
thus ( y in compactbelow x implies ( x >= y & y is compact ) ) :: thesis: ( x >= y & y is compact implies y in compactbelow x )

proof

assume y in compactbelow x ; :: thesis: ( x >= y & y is compact )
then ex z being Element of L st
( z = y & x >= z & z is compact ) ;
hence ( x >= y & y is compact ) ; :: thesis: verum

end;

assume ( x >= y & y is compact ) ; :: thesis: y in compactbelow x
hence y in compactbelow x ; :: thesis: verum