let V be strict RealUnitarySpace; :: thesis: ((Omega). V) /\ ((Omega). V) = V
thus ((Omega). V) /\ ((Omega). V) = (Omega). V by Th20
.= V by RUSUB_1:def 3 ; :: thesis: verum