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

then ( (A \/ B) ^Foi = A \/ B & A ^Foi = A ) ;

hence (A ^Foi) \/ (B ^Foi) = (A \/ B) ^Foi by A5; :: thesis: verum

(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

A5:
for C being Subset of FMT holds C = C ^Foi
by A1, A3, Th36;
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

end;for y being Element of FMT st y in C holds

y in C ^Foi

proof

hence
C c= C ^Foi
; :: thesis: verum
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;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

then ( (A \/ B) ^Foi = A \/ B & A ^Foi = A ) ;

hence (A ^Foi) \/ (B ^Foi) = (A \/ B) ^Foi by A5; :: thesis: verum