let L be non empty reflexive RelStr ; :: thesis: ( L is trivial implies ( L is complete & L is transitive & L is antisymmetric ) )
consider x being Element of L;
assume A1: for x, y being Element of L holds x = y ; :: according to STRUCT_0:def 10 :: thesis: ( L is complete & L is transitive & L is antisymmetric )
thus L is complete :: thesis: ( L is transitive & L is antisymmetric )

proof

let X be set ; :: according to LATTICE3:def 12 :: thesis: ex b₁ being Element of the carrier of L st
( X is_<=_than b₁ & ( for b₂ being Element of the carrier of L holds
( not X is_<=_than b₂ or b₁ <= b₂ ) ) )
take x ; :: thesis: ( X is_<=_than x & ( for b₁ being Element of the carrier of L holds
( not X is_<=_than b₁ or x <= b₁ ) ) )
thus for y being Element of L st y in X holds
y <= x by A1; :: according to LATTICE3:def 9 :: thesis: for b₁ being Element of the carrier of L holds
( not X is_<=_than b₁ or x <= b₁ )
let y be Element of L; :: thesis: ( not X is_<=_than y or x <= y )
y = x by A1;
hence ( not X is_<=_than y or x <= y ) by ORDERS_2:24; :: thesis: verum

end;

thus L is transitive :: thesis: L is antisymmetric

proof

let x, y, z be Element of L; :: according to YELLOW_0:def 2 :: thesis: ( x <= y & y <= z implies x <= z )
thus ( x <= y & y <= z implies x <= z ) by A1; :: thesis: verum

end;

let x be Element of L; :: according to YELLOW_0:def 3 :: thesis: for y being Element of L st x <= y & y <= x holds
x = y
thus for y being Element of L st x <= y & y <= x holds
x = y by A1; :: thesis: verum