set W = W1 .append W2;

now :: thesis: W1 .append W2 is closed end;

hence
W1 .append W2 is closed
; :: thesis: verumper cases
( W1 .last() = W2 .first() or W1 .last() <> W2 .first() )
;

end;

suppose A1:
W1 .last() = W2 .first()
; :: thesis: W1 .append W2 is closed

then
W1 .last() = W2 .last()
by Def24;

then W1 .first() = W2 .last() by Def24

.= (W1 .append W2) .last() by A1, Lm11 ;

then (W1 .append W2) .first() = (W1 .append W2) .last() by A1, Lm11;

hence W1 .append W2 is closed ; :: thesis: verum

end;then W1 .first() = W2 .last() by Def24

.= (W1 .append W2) .last() by A1, Lm11 ;

then (W1 .append W2) .first() = (W1 .append W2) .last() by A1, Lm11;

hence W1 .append W2 is closed ; :: thesis: verum