now

let a, b be set ; :: thesis: ( a c= b & b in compactbelow x implies a in compactbelow x )
assume A1: ( a c= b & b in compactbelow x ) ; :: thesis: a in compactbelow x
then b in { y where y is finite Subset of x : verum } by Th31;
then consider b1 being finite Subset of x such that
A2: b = b1 ;
a is finite Subset of x by A1, A2, 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 ( a in compactbelow x & b in compactbelow x ) ; :: thesis: a \/ b in compactbelow x
then A4: ( a in { y where y is finite Subset of x : verum } & b in { y where y is finite Subset of x : verum } ) by Th31;
then consider a1 being finite Subset of x such that
A5: a = a1 ;
consider b1 being finite Subset of x such that
A6: b = b1 by A4;
a \/ b is finite Subset of x by A5, 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