let T be TopStruct ; :: thesis: for M being Subset of T
for F, G being Subset-Family of T st F c= G holds
F | M c= G | M
let M be Subset of T; :: thesis: for F, G being Subset-Family of T st F c= G holds
F | M c= G | M
let F, G be Subset-Family of T; :: thesis: ( F c= G implies F | M c= G | M )
assume A1: F c= G ; :: thesis: F | M c= G | M
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F | M or x in G | M )
assume A2: x in F | M ; :: thesis: x in G | M
then reconsider X = x as Subset of (T | M) ;
ex R being Subset of T st
( R in F & R /\ M = X ) by A2, Def3;
hence x in G | M by A1, Def3; :: thesis: verum