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