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

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