ex Y being non empty Poset st
( Y is strict & Y is disconnected & Y is discrete )

proof

reconsider A = RelStr(# {1,2},(id {1,2}) #) as non empty Poset ;
reconsider A = A as non empty discrete Poset by Def1;
take A ; :: thesis: ( A is strict & A is disconnected & A is discrete )
ex a, b being Element of A st a <> b

proof

set a = 1;
set b = 2;
reconsider a = 1, b = 2 as Element of A by TARSKI:def 2;
take a ; :: thesis: ex b being Element of A st a <> b
take b ; :: thesis: a <> b
thus a <> b ; :: thesis: verum

end;

hence ( A is strict & A is disconnected & A is discrete ) by Th5; :: thesis: verum

end;

hence ex b₁ being non empty Poset st
( b₁ is strict & b₁ is disconnected & b₁ is discrete ) ; :: thesis: verum