ex Y being non empty Poset st

( Y is strict & Y is disconnected & Y is discrete )_{1} being non empty Poset st

( b_{1} is strict & b_{1} is disconnected & b_{1} is discrete )
; :: thesis: verum

( Y is strict & Y is disconnected & Y is discrete )

proof

hence
ex b
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

end;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

hence
( A is strict & A is disconnected & A is discrete )
by Th5; :: thesis: verum
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;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

( b