let SFX, SFY be set ; :: thesis: ( SFY <> {} & SFY is_coarser_than SFX implies meet SFX c= meet SFY )
assume that
A1: SFY <> {} and
A2: for Z2 being set st Z2 in SFY holds
ex Z1 being set st
( Z1 in SFX & Z1 c= Z2 ) ; :: according to SETFAM_1:def 3 :: thesis: meet SFX c= meet SFY
meet SFX c= meet SFY
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet SFX or x in meet SFY )
assume A3: x in meet SFX ; :: thesis: x in meet SFY
for Z being set st Z in SFY holds
x in Z
proof
let Z be set ; :: thesis: ( Z in SFY implies x in Z )
assume Z in SFY ; :: thesis: x in Z
then consider Z1 being set such that
A4: Z1 in SFX and
A5: Z1 c= Z by A2;
x in Z1 by A3, A4, Def1;
hence x in Z by A5; :: thesis: verum
end;
hence x in meet SFY by A1, Def1; :: thesis: verum
end;
hence meet SFX c= meet SFY ; :: thesis: verum