0 in {0} by TARSKI:def 1;
then reconsider r = {[0,0]} as Relation of {0} by RELSET_1:3;
reconsider T = RelStr(# {0},r #) as non empty RelStr ;
take T ; :: thesis:
thus T is reflexive :: thesis:

let x be Element of T; :: according to YELLOW_0:def 1 :: thesis:
x = 0 by TARSKI:def 1;
then [x,x] in {[0,0]} by TARSKI:def 1;
hence x <= x by ORDERS_2:def 5; :: thesis:

end;

then reconsider T9 = T as 1 -element reflexive RelStr ;
reconsider T99 = T9 as LATTICE ;
T9 is transitive ;
hence T is transitive ; :: thesis:
T9 is antisymmetric ;
hence T is antisymmetric ; :: thesis:
T9 is with_suprema ;
hence T is with_suprema ; :: thesis:
T9 is with_infima ;
hence T is with_infima ; :: thesis:
T99 is lower-bounded ;
hence T is lower-bounded ; :: thesis:
thus T is 1 -element ; :: thesis:
thus T is finite ; :: thesis:
thus T is strict ; :: thesis: