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 and
A2: x >= z' and
A3: z' is compact ;
z' << z' by A3, WAYBEL_3:def 2;
then z' << x by A2, 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