let R be RelStr ; :: thesis: for T1 being TopAugmentation of R
for T2 being TopAugmentation of T1 holds T2 is TopAugmentation of R
let T1 be TopAugmentation of R; :: thesis: for T2 being TopAugmentation of T1 holds T2 is TopAugmentation of R
let T2 be TopAugmentation of T1; :: thesis: T2 is TopAugmentation of R
thus RelStr(# the carrier of T2, the InternalRel of T2 #) = RelStr(# the carrier of T1, the InternalRel of T1 #) by Def4
.= RelStr(# the carrier of R, the InternalRel of R #) by Def4 ; :: according to YELLOW_9:def 4 :: thesis: verum