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

A1: X c= meet {X}

then meet {X} c= X by Th3;

hence meet {X} = X by A1; :: thesis: verum

A1: X c= meet {X}

proof

X in {X}
by TARSKI:def 1;
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;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

then meet {X} c= X by Th3;

hence meet {X} = X by A1; :: thesis: verum