now

let a, b be set ; :: thesis: ( a c= b & b in compactbelow x implies a in compactbelow x )
assume that
A1: a c= b and
A2: b in compactbelow x ; :: thesis: a in compactbelow x
b in { y where y is finite Subset of x : verum } by A2, Th31;
then ex b1 being finite Subset of x st b = b1 ;
then a is finite Subset of x by A1, XBOOLE_1:1;
then a in { y where y is finite Subset of x : verum } ;
hence a in compactbelow x by Th31; :: thesis: verum

end;

hence A3: compactbelow x is lower by WAYBEL_7:10; :: thesis: compactbelow x is directed

now

let a, b be set ; :: thesis: ( a in compactbelow x & b in compactbelow x implies a \/ b in compactbelow x )
assume that
A4: a in compactbelow x and
A5: b in compactbelow x ; :: thesis: a \/ b in compactbelow x
b in { y where y is finite Subset of x : verum } by A5, Th31;
then A6: ex b1 being finite Subset of x st b = b1 ;
a in { y where y is finite Subset of x : verum } by A4, Th31;
then ex a1 being finite Subset of x st a = a1 ;
then a \/ b is finite Subset of x by A6, XBOOLE_1:8;
then a \/ b in { y where y is finite Subset of x : verum } ;
hence a \/ b in compactbelow x by Th31; :: thesis: verum

end;

hence compactbelow x is directed by A3, WAYBEL_7:12; :: thesis: verum