let FMT be non empty FMT_Space_Str ; :: thesis: for A, B being Subset of FMT st FMT is Fo_filled & ( for x being Element of FMT holds {x} in U_FMT x ) holds
(A ^Foi) \/ (B ^Foi) = (A \/ B) ^Foi
let A, B be Subset of FMT; :: thesis: ( FMT is Fo_filled & ( for x being Element of FMT holds {x} in U_FMT x ) implies (A ^Foi) \/ (B ^Foi) = (A \/ B) ^Foi )
assume A1: FMT is Fo_filled ; :: thesis: ( ex x being Element of FMT st not {x} in U_FMT x or (A ^Foi) \/ (B ^Foi) = (A \/ B) ^Foi )
assume A2: for x being Element of FMT holds {x} in U_FMT x ; :: thesis: (A ^Foi) \/ (B ^Foi) = (A \/ B) ^Foi
A3: for C being Subset of FMT holds C c= C ^Foi
proof
let C be Subset of FMT; :: thesis: C c= C ^Foi
for y being Element of FMT st y in C holds
y in C ^Foi
proof
let y be Element of FMT; :: thesis: ( y in C implies y in C ^Foi )
assume y in C ; :: thesis: y in C ^Foi
then A4: {y} is Subset of C by SUBSET_1:41;
{y} in U_FMT y by A2;
hence y in C ^Foi by A4; :: thesis: verum
end;
hence C c= C ^Foi ; :: thesis: verum
end;
A5: for C being Subset of FMT holds C = C ^Foi by A1, A3, Th36;
then ( (A \/ B) ^Foi = A \/ B & A ^Foi = A ) ;
hence (A ^Foi) \/ (B ^Foi) = (A \/ B) ^Foi by A5; :: thesis: verum