consider f1, f2 being FinSequence of (TOP-REAL 2) such that
A1:
f1 is being_S-Seq
and
A2:
f2 is being_S-Seq
and
A3:
R^2-unit_square = (L~ f1) \/ (L~ f2)
and
A4:
(L~ f1) /\ (L~ f2) = {|[0,0]|,|[1,1]|}
and
f1 /. 1 = |[0,0]|
and
f1 /. (len f1) = |[1,1]|
and
f2 /. 1 = |[0,0]|
and
f2 /. (len f2) = |[1,1]|
by Th24;
reconsider P1 = L~ f1, P2 = L~ f2 as non empty Subset of (TOP-REAL 2) by A4;
take
P1
; 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
; ( 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, A2, A3, A4; verum