set T = TrivLattRelStr ;
set C = the carrier of TrivLattRelStr;
set I = the InternalRel of TrivLattRelStr;
field the InternalRel of TrivLattRelStr = the carrier of TrivLattRelStr by PARTIT_2:18;
then the InternalRel of TrivLattRelStr is_reflexive_in the carrier of TrivLattRelStr by RELAT_2:def 9;
hence TrivLattRelStr is reflexive by ORDERS_2:def 2; :: thesis: verum