0 in {0 } by TARSKI:def 1;
then reconsider r = {[0 ,0 ]} as Relation of {0 } by RELSET_1:8;
reconsider T = RelStr(# {0 },r #) as non empty RelStr ;
take T ; :: thesis: ( T is trivial & T is reflexive & T is transitive & T is antisymmetric & T is with_suprema & T is with_infima & T is lower-bounded & not T is empty & T is finite & T is strict )
thus T is trivial ; :: thesis: ( T is reflexive & T is transitive & T is antisymmetric & T is with_suprema & T is with_infima & T is lower-bounded & not T is empty & T is finite & T is strict )
thus T is reflexive :: thesis: ( T is transitive & T is antisymmetric & T is with_suprema & T is with_infima & T is lower-bounded & not T is empty & T is finite & T is strict )

proof

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

end;

then reconsider T' = T as non empty trivial reflexive RelStr ;
T' is transitive ;
hence T is transitive ; :: thesis: ( T is antisymmetric & T is with_suprema & T is with_infima & T is lower-bounded & not T is empty & T is finite & T is strict )
T' is antisymmetric ;
hence T is antisymmetric ; :: thesis: ( T is with_suprema & T is with_infima & T is lower-bounded & not T is empty & T is finite & T is strict )
T' is with_suprema ;
hence T is with_suprema ; :: thesis: ( T is with_infima & T is lower-bounded & not T is empty & T is finite & T is strict )
T' is with_infima ;
hence T is with_infima ; :: thesis: ( T is lower-bounded & not T is empty & T is finite & T is strict )
reconsider T'' = T' as LATTICE ;
T'' is lower-bounded ;
hence T is lower-bounded ; :: thesis: ( not T is empty & T is finite & T is strict )
thus not T is empty ; :: thesis: ( T is finite & T is strict )
thus T is finite ; :: thesis: T is strict
thus T is strict ; :: thesis: verum