let L be non empty reflexive transitive RelStr ; :: thesis: for x being Element of L holds compactbelow x c= waybelow x
let x be Element of L; :: thesis: compactbelow x c= waybelow x

now

let z be set ; :: thesis: ( z in compactbelow x implies z in waybelow x )
assume z in compactbelow x ; :: thesis: z in waybelow x
then consider z' being Element of L such that
A1: ( z' = z & x >= z' & z' is compact ) ;
z' << z' by A1, WAYBEL_3:def 2;
then z' << x by A1, WAYBEL_3:2;
hence z in waybelow x by A1, WAYBEL_3:7; :: thesis: verum

end;

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