reconsider Z = the carrier of (Lin Y) as Subset of X by RLSUB_1:def 2;
reconsider T = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),X)),(Add_ ((Cl Z),X)),(Mult_ ((Cl Z),X)),(Norm_ ((Cl Z),X)) #) as non empty NORMSTR by LMCL1;
ex Z being Subset of X st
( Z = the carrier of (Lin Y) & T = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),X)),(Add_ ((Cl Z),X)),(Mult_ ((Cl Z),X)),(Norm_ ((Cl Z),X)) #) )
;
hence
( ex b1 being non empty NORMSTR ex Z being Subset of X st
( Z = the carrier of (Lin Y) & b1 = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),X)),(Add_ ((Cl Z),X)),(Mult_ ((Cl Z),X)),(Norm_ ((Cl Z),X)) #) ) & ( for b1, b2 being non empty NORMSTR st ex Z being Subset of X st
( Z = the carrier of (Lin Y) & b1 = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),X)),(Add_ ((Cl Z),X)),(Mult_ ((Cl Z),X)),(Norm_ ((Cl Z),X)) #) ) & ex Z being Subset of X st
( Z = the carrier of (Lin Y) & b2 = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),X)),(Add_ ((Cl Z),X)),(Mult_ ((Cl Z),X)),(Norm_ ((Cl Z),X)) #) ) holds
b1 = b2 ) )
; verum