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
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;