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

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

hence
meet SFX c= meet SFY
; :: thesis: verum
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

end;assume A3: x in meet SFX ; :: thesis: x in meet SFY

for Z being set st Z in SFY holds

x in Z

proof

hence
x in meet SFY
by A1, Def1; :: thesis: verum
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;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