let V be RealUnitarySpace; :: thesis: for M being non empty Subset of V holds Ort_Comp M = Ort_Comp (Ort_Comp (Ort_Comp M))
let M be non empty Subset of V; :: thesis: Ort_Comp M = Ort_Comp (Ort_Comp (Ort_Comp M))
set N = the carrier of (Ort_Comp M);
reconsider N = the carrier of (Ort_Comp M) as Subset of V by RUSUB_1:def 1;
reconsider N = N as non empty Subset of V ;
set L = the carrier of (Ort_Comp (Ort_Comp M));
reconsider L = the carrier of (Ort_Comp (Ort_Comp M)) as Subset of V by RUSUB_1:def 1;
reconsider L = L as non empty Subset of V ;
N c= the carrier of (Ort_Comp (Ort_Comp N)) by Th25;
then A1: N c= the carrier of (Ort_Comp (Ort_Comp (Ort_Comp M))) by Th27;
the carrier of (Ort_Comp L) c= the carrier of (Ort_Comp M) by Th25, Th26;
then the carrier of (Ort_Comp (Ort_Comp (Ort_Comp M))) c= the carrier of (Ort_Comp M) by Th27;
then the carrier of (Ort_Comp (Ort_Comp (Ort_Comp M))) = the carrier of (Ort_Comp M) by A1;
hence Ort_Comp M = Ort_Comp (Ort_Comp (Ort_Comp M)) by RUSUB_1:24; :: thesis: verum