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 :: thesis: for z being object st z in compactbelow x holds
z in compactbelow y
let z be object ; :: 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 z9 being Element of L such that
A2: z9 = z and
A3: x >= z9 and
A4: z9 is compact ;
z9 <= y by A1, A3, ORDERS_2:3;
hence z in compactbelow y by A2, A4, WAYBEL_8:4; :: thesis: verum
end;
hence compactbelow x c= compactbelow y ; :: thesis: verum