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