thus (W .remove (m,n)) .first() = W .first() by Lm33
.= W .last() by Def24
.= (W .remove (m,n)) .last() by Lm33 ; :: according to GLIB_001:def 24 :: thesis: verum