set W = W1 .append W2;

now :: thesis: W1 .append W2 is closed

per cases ( W1 .last() = W2 .first() or W1 .last() <> W2 .first() ) ;

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;

suppose W1 .last() <> W2 .first() ; :: thesis: W1 .append W2 is closed

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

end;

end;

end;

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