now :: thesis: for a, b being set st a c= b & b in compactbelow x holds
a in compactbelow x

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, Th29;
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 Th29; :: thesis: verum

end;

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

now :: thesis: for a, b being set st a in compactbelow x & b in compactbelow x holds
a \/ b in compactbelow x

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, Th29;
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, Th29;
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 Th29; :: thesis: verum

end;

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