Help declaring Huntington postulates

Stream: new members

[JULIÁN CALDERÓN ALMENDROS]

I am new by these lands. Excuse me, please, if I make many mistakes. I'm trying to prove some lemmas about boolean algebras.
I declare 'setB' as a Set type. The 1904 Huntington's Postulates, I declare them as H1s, H1p,..., H5, H6 as of Props type. How I declare 'e' as element of 'setB'?

[Notification Bot]

A message was moved here from #general > Lean 4 project blueprint by Mario Carneiro.

[Eric Wieser]

Can you give a #mwe?