consider x being Element of (MonSet L) such that
A1: x is_>=_than the carrier of (MonSet L) by Lm6;
take x ; :: according to YELLOW_0:def 5 :: thesis: the carrier of (MonSet L) is_<=_than x
thus the carrier of (MonSet L) is_<=_than x by A1; :: thesis: verum