set s = the set ;
set D = { the set };
set R = the Order of { the set };
take A = RelStr(# { the set }, the Order of { the set } #); :: thesis:
thus A is strict ; :: thesis:

hereby :: according to LATTICE3:def 12 :: thesis:

let X be set ; :: thesis:
reconsider s = the set as Element of A by TARSKI:def 1;
take s = s; :: thesis:
thus X is_<=_than s :: thesis:

let a be Element of A; :: according to LATTICE3:def 9 :: thesis:
assume a in X ; :: thesis:
thus a <= s by TARSKI:def 1; :: thesis:

end;

let b be Element of A; :: thesis:
assume X is_<=_than b ; :: thesis:
thus s <= b by TARSKI:def 1; :: thesis:

end;

thus not A is empty ; :: thesis: