let I be set ; :: thesis: for M being ManySortedSet of
for SH, SF, SG being MSSubsetFamily of M st SH = SF \/ SG holds
meet SH = (meet SF) /\ (meet SG)
let M be ManySortedSet of ; :: thesis: for SH, SF, SG being MSSubsetFamily of M st SH = SF \/ SG holds
meet SH = (meet SF) /\ (meet SG)
let SH, SF, SG be MSSubsetFamily of M; :: thesis: ( SH = SF \/ SG implies meet SH = (meet SF) /\ (meet SG) )
assume A1: SH = SF \/ SG ; :: thesis: meet SH = (meet SF) /\ (meet SG)

now

let i be set ; :: thesis: ( i in I implies (meet SH) . i = ((meet SF) /\ (meet SG)) . i )
assume A2: i in I ; :: thesis: (meet SH) . i = ((meet SF) /\ (meet SG)) . i
then consider Qf being Subset-Family of (M . i) such that
A3: Qf = SF . i and
A4: (meet SF) . i = Intersect Qf by Def2;
consider Qg being Subset-Family of (M . i) such that
A5: Qg = SG . i and
A6: (meet SG) . i = Intersect Qg by A2, Def2;
consider Qh being Subset-Family of (M . i) such that
A7: Qh = SH . i and
A8: (meet SH) . i = Intersect Qh by A2, Def2;
A9: Qh = Qf \/ Qg by A1, A2, A3, A5, A7, PBOOLE:def 7;

now

per cases ( ( Qf <> {} & Qg <> {} ) or ( Qf <> {} & Qg = {} ) or ( Qf = {} & Qg <> {} ) or ( Qf = {} & Qg = {} ) ) ;

case A10: ( Qf <> {} & Qg <> {} ) ; :: thesis: (meet SH) . i = ((meet SF) /\ (meet SG)) . i

then Qh <> {} by A9;
hence (meet SH) . i = meet Qh by A8, SETFAM_1:def 10
.= (meet Qf) /\ (meet Qg) by A9, A10, SETFAM_1:10
.= ((meet SF) . i) /\ (meet Qg) by A4, A10, SETFAM_1:def 10
.= ((meet SF) . i) /\ ((meet SG) . i) by A6, A10, SETFAM_1:def 10
.= ((meet SF) /\ (meet SG)) . i by A2, PBOOLE:def 8 ;
:: thesis: verum

end;

case A11: ( Qf <> {} & Qg = {} ) ; :: thesis: (meet SH) . i = ((meet SF) /\ (meet SG)) . i

hence (meet SH) . i = ((meet SF) . i) /\ (M . i) by A4, A8, A9, XBOOLE_1:28
.= ((meet SF) . i) /\ ((meet SG) . i) by A6, A11, SETFAM_1:def 10
.= ((meet SF) /\ (meet SG)) . i by A2, PBOOLE:def 8 ;
:: thesis: verum

end;

case A12: ( Qf = {} & Qg <> {} ) ; :: thesis: (meet SH) . i = ((meet SF) /\ (meet SG)) . i

hence (meet SH) . i = (M . i) /\ ((meet SG) . i) by A6, A8, A9, XBOOLE_1:28
.= ((meet SF) . i) /\ ((meet SG) . i) by A4, A12, SETFAM_1:def 10
.= ((meet SF) /\ (meet SG)) . i by A2, PBOOLE:def 8 ;
:: thesis: verum

end;

case ( Qf = {} & Qg = {} ) ; :: thesis: (meet SH) . i = ((meet SF) /\ (meet SG)) . i

hence (meet SH) . i = (Intersect Qf) /\ (Intersect Qg) by A8, A9
.= ((meet SF) /\ (meet SG)) . i by A2, A4, A6, PBOOLE:def 8 ;
:: thesis: verum

end;

end;

end;

hence (meet SH) . i = ((meet SF) /\ (meet SG)) . i ; :: thesis: verum

end;

hence meet SH = (meet SF) /\ (meet SG) by PBOOLE:3; :: thesis: verum