begin
Lm1:
for F, G being ext-real-membered set st F c= G holds
-- F c= -- G
Lm2:
for A, B being complex-membered set st A c= B holds
-- A c= -- B
Lm3:
for A, B being complex-membered set st A c= B holds
A "" c= B ""
Lm4:
for F, G being ext-real-membered set holds -- (F ++ G) = (-- F) ++ (-- G)
Lm5:
for A, B being complex-membered set holds -- (A ++ B) = (-- A) ++ (-- B)