{A} is a_partition of A by EQREL_1:39;
then {A} in PARTITIONS A by PARTIT1:def 3;
then reconsider S = {{A}} as Subset of (PARTITIONS A) by ZFMISC_1:31;
take S ; :: thesis: for X, Y being a_partition of A st X in S & Y in S & not X is_finer_than Y holds
Y is_finer_than X
thus for X, Y being a_partition of A st X in S & Y in S & not X is_finer_than Y holds
Y is_finer_than X by Lm1; :: thesis: verum