reconsider F = {X} as Subset-Family of X by ZFMISC_1:68;

take F ; :: thesis: ( not F is empty & F is ordered )

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 F ; :: thesis: ( not F is empty & F is ordered )

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 ) ) ) )

proof

hence
( not F is empty & F is ordered )
; :: thesis: verum
take
X
; :: thesis: ex B being set st

( X in F & B in F & ( for Y being set holds

( Y in F iff ( X c= Y & Y c= B ) ) ) )

take X ; :: thesis: ( X in F & X in F & ( for Y being set holds

( Y in F iff ( X c= Y & Y c= X ) ) ) )

thus ( X in F & X in F ) by TARSKI:def 1; :: thesis: for Y being set holds

( Y in F iff ( X c= Y & Y c= X ) )

let Y be set ; :: thesis: ( Y in F iff ( X c= Y & Y c= X ) )

thus ( Y in F implies ( X c= Y & Y c= X ) ) by TARSKI:def 1; :: thesis: ( X c= Y & Y c= X implies Y in F )

assume ( X c= Y & Y c= X ) ; :: thesis: Y in F

then X = Y ;

hence Y in F by TARSKI:def 1; :: thesis: verum

end;( X in F & B in F & ( for Y being set holds

( Y in F iff ( X c= Y & Y c= B ) ) ) )

take X ; :: thesis: ( X in F & X in F & ( for Y being set holds

( Y in F iff ( X c= Y & Y c= X ) ) ) )

thus ( X in F & X in F ) by TARSKI:def 1; :: thesis: for Y being set holds

( Y in F iff ( X c= Y & Y c= X ) )

let Y be set ; :: thesis: ( Y in F iff ( X c= Y & Y c= X ) )

thus ( Y in F implies ( X c= Y & Y c= X ) ) by TARSKI:def 1; :: thesis: ( X c= Y & Y c= X implies Y in F )

assume ( X c= Y & Y c= X ) ; :: thesis: Y in F

then X = Y ;

hence Y in F by TARSKI:def 1; :: thesis: verum