let T1, T2 be non empty RelStr ; :: thesis: for S1 being non empty full SubRelStr of T1
for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is filtered-infs-inheriting holds
S2 is filtered-infs-inheriting
let S1 be non empty full SubRelStr of T1; :: thesis: for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is filtered-infs-inheriting holds
S2 is filtered-infs-inheriting
let S2 be non empty full SubRelStr of T2; :: thesis: ( RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is filtered-infs-inheriting implies S2 is filtered-infs-inheriting )
assume A1: RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) ; :: thesis: ( not the carrier of S1 = the carrier of S2 or not S1 is filtered-infs-inheriting or S2 is filtered-infs-inheriting )
RelStr(# the carrier of S2, the InternalRel of S2 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) ;
then reconsider R = S2 as full SubRelStr of T1 by A1, Th12;
assume A2: the carrier of S1 = the carrier of S2 ; :: thesis: ( not S1 is filtered-infs-inheriting or S2 is filtered-infs-inheriting )
then A3: RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_0:57;
assume A4: for X being filtered Subset of S1 st X <> {} & ex_inf_of X,T1 holds
"/\" (X,T1) in the carrier of S1 ; :: according to WAYBEL_0:def 3 :: thesis: S2 is filtered-infs-inheriting
let X be filtered Subset of S2; :: according to WAYBEL_0:def 3 :: thesis: ( X = {} or not ex_inf_of X,T2 or "/\" (X,T2) in the carrier of S2 )
assume A5: X <> {} ; :: thesis: ( not ex_inf_of X,T2 or "/\" (X,T2) in the carrier of S2 )
reconsider Y = X as filtered Subset of S1 by A3, WAYBEL_0:4;
assume A6: ex_inf_of X,T2 ; :: thesis: "/\" (X,T2) in the carrier of S2
then "/\" (Y,T1) in the carrier of S1 by A1, A4, A5, YELLOW_0:14;
hence "/\" (X,T2) in the carrier of S2 by A1, A2, A6, YELLOW_0:27; :: thesis: verum