let X be set ; :: thesis: meet {X} = X
A1: X c= meet {X}

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in X or y in meet {X} )
assume y in X ; :: thesis: y in meet {X}
then for Z being set st Z in {X} holds
y in Z by TARSKI:def 1;
hence y in meet {X} by Def1; :: thesis: verum

end;

X in {X} by TARSKI:def 1;
then meet {X} c= X by Th3;
hence meet {X} = X by A1; :: thesis: verum