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