let B be antichain; :: thesis: ( {} in B implies B = {{}} )
assume A1: {} in B ; :: thesis: B = {{}}
for a being object st a in B holds
a = {}

proof

let a be object ; :: thesis: ( a in B implies a = {} )
assume A3: a in B ; :: thesis: a = {}
then reconsider a = a as FinSequence ;
{} ^ a in B by A3, FINSEQ_1:34;
hence a = {} by A1, Def16; :: thesis: verum

end;

then for a being object holds
( a in B iff a = {} ) by A1;
hence B = {{}} by TARSKI:def 1; :: thesis: verum