consider f1, f2 being FinSequence of (TOP-REAL 2) such that
A1: ( f1 is being_S-Seq & f2 is being_S-Seq & R^2-unit_square = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {|[0 ,0 ]|,|[1,1]|} ) and
( f1 /. 1 = |[0 ,0 ]| & f1 /. (len f1) = |[1,1]| & f2 /. 1 = |[0 ,0 ]| & f2 /. (len f2) = |[1,1]| ) by Th30;
reconsider P1 = L~ f1, P2 = L~ f2 as non empty Subset of (TOP-REAL 2) by A1;
take P1 ; :: thesis: ex P2 being non empty Subset of (TOP-REAL 2) st
( P1 is being_S-P_arc & P2 is being_S-P_arc & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {|[0 ,0 ]|,|[1,1]|} )
take P2 ; :: thesis: ( P1 is being_S-P_arc & P2 is being_S-P_arc & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {|[0 ,0 ]|,|[1,1]|} )
thus ( P1 is being_S-P_arc & P2 is being_S-P_arc & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {|[0 ,0 ]|,|[1,1]|} ) by A1, Def11; :: thesis: verum