let L be 1 -element reflexive RelStr ; :: thesis: ( L is complete & L is transitive & L is antisymmetric )
set x = the Element of L;
A1: for x, y being Element of L holds x = y by STRUCT_0:def 10;
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 the Element of L ; :: thesis: ( X is_<=_than the Element of L & ( for b₁ being Element of the carrier of L holds
( not X is_<=_than b₁ or the Element of L <= b₁ ) ) )
thus for y being Element of L st y in X holds
y <= the Element of L by A1; :: according to LATTICE3:def 9 :: thesis: for b₁ being Element of the carrier of L holds
( not X is_<=_than b₁ or the Element of L <= b₁ )
let y be Element of L; :: thesis: ( not X is_<=_than y or the Element of L <= y )
y = the Element of L by A1;
hence ( not X is_<=_than y or the Element of L <= y ) by ORDERS_2:1; :: thesis: verum

end;

thus L is transitive by A1; :: thesis: L is antisymmetric
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