let X, Y be set ; :: thesis: ( X <> {} & X c= Y implies meet Y c= meet X )
assume that
A1: X <> {} and
A2: X c= Y ; :: thesis: meet Y c= meet X
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet Y or x in meet X )
assume x in meet Y ; :: thesis: x in meet X
then for Z being set st Z in X holds
x in Z by A2, Def1;
hence x in meet X by A1, Def1; :: thesis: verum