let L be non empty reflexive transitive RelStr ; :: thesis: for x, y being Element of L st x <= y holds
compactbelow x c= compactbelow y
let x, y be Element of L; :: thesis: ( x <= y implies compactbelow x c= compactbelow y )
assume A1: x <= y ; :: thesis: compactbelow x c= compactbelow y

now

let z be set ; :: thesis: ( z in compactbelow x implies z in compactbelow y )
assume z in compactbelow x ; :: thesis: z in compactbelow y
then z in { v where v is Element of L : ( x >= v & v is compact ) } by WAYBEL_8:def 2;
then consider z' being Element of L such that
A2: z' = z and
A3: x >= z' and
A4: z' is compact ;
z' <= y by A1, A3, ORDERS_2:26;
hence z in compactbelow y by A2, A4, WAYBEL_8:4; :: thesis: verum

end;

hence compactbelow x c= compactbelow y by TARSKI:def 3; :: thesis: verum