consider x being set ;
reconsider A = RelStr(# {x},(id {x}) #) as non empty Poset ;
[#] A = {x} ;
then not A is disconnected by Th4;
hence ex b₁ being non empty Poset st
( b₁ is strict & not b₁ is disconnected ) ; :: thesis: verum