reconsider F = {X} as Subset-Family of X by ZFMISC_1:68;
take F ; :: thesis:
ex A, B being set st
( A in F & B in F & ( for Y being set holds
( Y in F iff ( A c= Y & Y c= B ) ) ) )

take X ; :: thesis:
take X ; :: thesis:
thus ( X in F & X in F ) by TARSKI:def 1; :: thesis:
let Y be set ; :: thesis:
thus ( Y in F implies ( X c= Y & Y c= X ) ) by TARSKI:def 1; :: thesis:
assume ( X c= Y & Y c= X ) ; :: thesis:
then X = Y ;
hence Y in F by TARSKI:def 1; :: thesis:

end;