let SFX, SFY be set ; :: thesis: ( SFX is_finer_than SFY implies union SFX c= union SFY )

assume A1: for X being set st X in SFX holds

ex Y being set st

( Y in SFY & X c= Y ) ; :: according to SETFAM_1:def 2 :: thesis: union SFX c= union SFY

thus union SFX c= union SFY :: thesis: verum

assume A1: for X being set st X in SFX holds

ex Y being set st

( Y in SFY & X c= Y ) ; :: according to SETFAM_1:def 2 :: thesis: union SFX c= union SFY

thus union SFX c= union SFY :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union SFX or x in union SFY )

assume x in union SFX ; :: thesis: x in union SFY

then consider Y being set such that

A2: x in Y and

A3: Y in SFX by TARSKI:def 4;

ex Z being set st

( Z in SFY & Y c= Z ) by A1, A3;

hence x in union SFY by A2, TARSKI:def 4; :: thesis: verum

end;assume x in union SFX ; :: thesis: x in union SFY

then consider Y being set such that

A2: x in Y and

A3: Y in SFX by TARSKI:def 4;

ex Z being set st

( Z in SFY & Y c= Z ) by A1, A3;

hence x in union SFY by A2, TARSKI:def 4; :: thesis: verum