thus not [.r1,r2,r19,r29.] is empty ; :: thesis: [.r1,r2,r19,r29.] is compact
A1: (LSeg |[r2,r29]|,|[r2,r19]|) \/ (LSeg |[r2,r19]|,|[r1,r19]|) is compact by COMPTS_1:19;
(LSeg |[r1,r19]|,|[r1,r29]|) \/ (LSeg |[r1,r29]|,|[r2,r29]|) is compact by COMPTS_1:19;
hence [.r1,r2,r19,r29.] is compact by A1, COMPTS_1:19; :: thesis: verum