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: ( A is strict & A is complete & not A is empty )
thus A is strict ; :: thesis: ( A is complete & not A is empty )

hereby :: according to LATTICE3:def 12 :: thesis: not A is empty

let X be set ; :: thesis: ex s being Element of A st
( X is_<=_than s & ( for b being Element of A st X is_<=_than b holds
s <= b ) )
reconsider s = the set as Element of A by TARSKI:def 1;
take s = s; :: thesis: ( X is_<=_than s & ( for b being Element of A st X is_<=_than b holds
s <= b ) )
thus X is_<=_than s :: thesis: for b being Element of A st X is_<=_than b holds
s <= b

proof

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

end;

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

end;

thus not A is empty ; :: thesis: verum