let n be Nat; :: thesis: for X being set
for A1, A2 being SetSequence of X holds ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence (A1 (\/) A2)) . n
let X be set ; :: thesis: for A1, A2 being SetSequence of X holds ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence (A1 (\/) A2)) . n
let A1, A2 be SetSequence of X; :: thesis: ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence (A1 (\/) A2)) . n
A1: Intersection ((A1 ^\ n) (\/) (A2 ^\ n)) = Intersection ((A1 (\/) A2) ^\ n) by Th5
.= (inferior_setsequence (A1 (\/) A2)) . n by Th1 ;
((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) = (Intersection (A1 ^\ n)) \/ ((inferior_setsequence A2) . n) by Th1
.= (Intersection (A1 ^\ n)) \/ (Intersection (A2 ^\ n)) by Th1 ;
hence ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence (A1 (\/) A2)) . n by A1, Th13; :: thesis: verum