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 :: thesis: for z being object st z in compactbelow x holds
z in waybelow x

let z be object ; :: thesis: ( z in compactbelow x implies z in waybelow x )
assume z in compactbelow x ; :: thesis: z in waybelow x
then consider z9 being Element of L such that
A1: z9 = z and
A2: x >= z9 and
A3: z9 is compact ;
z9 << z9 by A3, WAYBEL_3:def 2;
then z9 << 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 ; :: thesis: verum