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

proof

let y be set ; :: 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 Th4;
hence meet {x} = x by A1, XBOOLE_0:def 10; :: thesis: verum