let T be TopSpace; :: thesis: for A, B being Subset of T st A is 1st_class & B is 1st_class holds

( (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) & (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) )

let A, B be Subset of T; :: thesis: ( A is 1st_class & B is 1st_class implies ( (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) & (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) ) )

assume that

A1: A is 1st_class and

A2: B is 1st_class ; :: thesis: ( (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) & (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) )

A3: Cl (Int B) = Cl (Int (Cl B)) by A2, Th41;

Cl (Int A) = Cl (Int (Cl A)) by A1, Th41;

then A4: (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (Cl (A \/ B))) by A3, Th2;

Int (Cl (A /\ B)) c= Int ((Cl A) /\ (Cl B)) by PRE_TOPC:21, TOPS_1:19;

then A5: Int (Cl (A /\ B)) c= (Int (Cl A)) /\ (Int (Cl B)) by TOPS_1:17;

Int (A \/ B) c= Int (Cl (A \/ B)) by PRE_TOPC:18, TOPS_1:19;

then A6: Cl (Int (A \/ B)) c= Cl (Int (Cl (A \/ B))) by PRE_TOPC:19;

Cl ((Int A) \/ (Int B)) c= Cl (Int (A \/ B)) by PRE_TOPC:19, TOPS_1:20;

then A7: (Cl (Int A)) \/ (Cl (Int B)) c= Cl (Int (A \/ B)) by PRE_TOPC:20;

A8: Int (Cl B) = Int (Cl (Int B)) by A2, Th41;

Cl (Int (A /\ B)) c= Cl (A /\ B) by PRE_TOPC:19, TOPS_1:16;

then A9: Int (Cl (Int (A /\ B))) c= Int (Cl (A /\ B)) by TOPS_1:19;

Int (Cl A) = Int (Cl (Int A)) by A1, Th41;

then (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (Int (A /\ B))) by A8, Th1;

hence ( (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) & (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) ) by A5, A9, A7, A4, A6, XBOOLE_0:def 10; :: thesis: verum

( (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) & (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) )

let A, B be Subset of T; :: thesis: ( A is 1st_class & B is 1st_class implies ( (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) & (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) ) )

assume that

A1: A is 1st_class and

A2: B is 1st_class ; :: thesis: ( (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) & (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) )

A3: Cl (Int B) = Cl (Int (Cl B)) by A2, Th41;

Cl (Int A) = Cl (Int (Cl A)) by A1, Th41;

then A4: (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (Cl (A \/ B))) by A3, Th2;

Int (Cl (A /\ B)) c= Int ((Cl A) /\ (Cl B)) by PRE_TOPC:21, TOPS_1:19;

then A5: Int (Cl (A /\ B)) c= (Int (Cl A)) /\ (Int (Cl B)) by TOPS_1:17;

Int (A \/ B) c= Int (Cl (A \/ B)) by PRE_TOPC:18, TOPS_1:19;

then A6: Cl (Int (A \/ B)) c= Cl (Int (Cl (A \/ B))) by PRE_TOPC:19;

Cl ((Int A) \/ (Int B)) c= Cl (Int (A \/ B)) by PRE_TOPC:19, TOPS_1:20;

then A7: (Cl (Int A)) \/ (Cl (Int B)) c= Cl (Int (A \/ B)) by PRE_TOPC:20;

A8: Int (Cl B) = Int (Cl (Int B)) by A2, Th41;

Cl (Int (A /\ B)) c= Cl (A /\ B) by PRE_TOPC:19, TOPS_1:16;

then A9: Int (Cl (Int (A /\ B))) c= Int (Cl (A /\ B)) by TOPS_1:19;

Int (Cl A) = Int (Cl (Int A)) by A1, Th41;

then (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (Int (A /\ B))) by A8, Th1;

hence ( (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) & (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) ) by A5, A9, A7, A4, A6, XBOOLE_0:def 10; :: thesis: verum