let X be set ; :: thesis: for Si being SigmaField of X
for S3, S1, S2 being SetSequence of st ( for n being Element of NAT holds S3 . n = (S1 . n) \/ (S2 . n) ) holds
(lim_inf S1) \/ (lim_inf S2) c= lim_inf S3
let Si be SigmaField of X; :: thesis: for S3, S1, S2 being SetSequence of st ( for n being Element of NAT holds S3 . n = (S1 . n) \/ (S2 . n) ) holds
(lim_inf S1) \/ (lim_inf S2) c= lim_inf S3
let S3, S1, S2 be SetSequence of ; :: thesis: ( ( for n being Element of NAT holds S3 . n = (S1 . n) \/ (S2 . n) ) implies (lim_inf S1) \/ (lim_inf S2) c= lim_inf S3 )
assume A0: for n being Element of NAT holds S3 . n = (S1 . n) \/ (S2 . n) ; :: thesis: (lim_inf S1) \/ (lim_inf S2) c= lim_inf S3
for A3, B, A2 being SetSequence of X st ( for n being Element of NAT holds A3 . n = (B . n) \/ (A2 . n) ) holds
(Union (inferior_setsequence B)) \/ (Union (inferior_setsequence A2)) c= Union (inferior_setsequence A3)

proof

let A3, B, A2 be SetSequence of X; :: thesis: ( ( for n being Element of NAT holds A3 . n = (B . n) \/ (A2 . n) ) implies (Union (inferior_setsequence B)) \/ (Union (inferior_setsequence A2)) c= Union (inferior_setsequence A3) )
assume B0: for n being Element of NAT holds A3 . n = (B . n) \/ (A2 . n) ; :: thesis: (Union (inferior_setsequence B)) \/ (Union (inferior_setsequence A2)) c= Union (inferior_setsequence A3)
B1: lim_inf B = Union (inferior_setsequence B) ;
B2: lim_inf A2 = Union (inferior_setsequence A2) ;
lim_inf A3 = Union (inferior_setsequence A3) ;
hence (Union (inferior_setsequence B)) \/ (Union (inferior_setsequence A2)) c= Union (inferior_setsequence A3) by B0, B1, B2, KURATO_2:15; :: thesis: verum

end;

hence (lim_inf S1) \/ (lim_inf S2) c= lim_inf S3 by A0; :: thesis: verum