for Y being Element of SM holds Y = union { s where s is Element of S : ( s in {} & s c= Y ) }

let Y be Element of SM; :: thesis:
A2: Y = {} by A1, SUBSET_1:def 1;
union { s where s is Element of S : ( s in {} & s c= Y ) } c= {}

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in union { s where s is Element of S : ( s in {} & s c= Y ) } ; :: thesis:
then consider y being set such that
x in y and
A3: y in { s where s is Element of S : ( s in {} & s c= Y ) } by TARSKI:def 4;
consider s being Element of S such that
y = s and
A4: s in {} and
s c= Y by A3;
thus x in {} by A4; :: thesis:

end;

hence Y = union { s where s is Element of S : ( s in {} & s c= Y ) } by A2; :: thesis:

end;

hence ex P being finite Subset of S st
( P is a_partition of union SM & ( for Y being Element of SM holds Y = union { s where s is Element of S : ( s in P & s c= Y ) } ) ) by A1, ZFMISC_1:2, EQREL_1:45; :: thesis:

end;

consider FSM being FinSequence such that
A6: SM = rng FSM by FINSEQ_1:52;
FSM is FinSequence of S by A6, FINSEQ_1:def 4;
then consider P being finite Subset of S such that
A7: P is a_partition of Union FSM and
A8: for n being Nat st n in dom FSM holds
FSM . n = union { s where s is Element of S : ( s in P & s c= FSM . n ) } by Lem10;
for Y being Element of SM holds Y = union { s where s is Element of S : ( s in P & s c= Y ) }

let Y be Element of SM; :: thesis:
consider i being object such that
A9: i in dom FSM and
A10: Y = FSM . i by A5, A6, FUNCT_1:def 3;
thus Y c= union { s where s is Element of S : ( s in P & s c= Y ) } by A9, A10, A8; :: according to XBOOLE_0:def 10 :: thesis:
thus union { s where s is Element of S : ( s in P & s c= Y ) } c= Y by A9, A10, A8; :: thesis:

end;

hence ex P being finite Subset of S st
( P is a_partition of union SM & ( for Y being Element of SM holds Y = union { s where s is Element of S : ( s in P & s c= Y ) } ) ) by A6, A7; :: thesis:

end;