let Y1, Y2 be Subset of [:S,the carrier of A:]; :: thesis: ( [:S,(ElementaryInstructions A):] c= Y1 & [:S,{(EmptyIns A)}:] c= Y1 & ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in Y1 & [(f . s,I),J] in Y1 implies [s,(I \; J)] in Y1 ) & ( [s,C] in Y1 & [(f . s,C),I] in Y1 & f . s,C in T implies [s,(if-then-else C,I,J)] in Y1 ) & ( [s,C] in Y1 & [(f . s,C),J] in Y1 & f . s,C nin T implies [s,(if-then-else C,I,J)] in Y1 ) & ( [s,C] in Y1 & ex r being non empty FinSequence of S st
( r . 1 = f . s,C & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in Y1 & r . (i + 1) = f . (r . i),(I \; C) ) ) ) implies [s,(while C,I)] in Y1 ) ) ) & ( for P being Subset of [:S,the carrier of A:] st [:S,(ElementaryInstructions A):] c= P & [:S,{(EmptyIns A)}:] c= P & ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in P & [(f . s,I),J] in P implies [s,(I \; J)] in P ) & ( [s,C] in P & [(f . s,C),I] in P & f . s,C in T implies [s,(if-then-else C,I,J)] in P ) & ( [s,C] in P & [(f . s,C),J] in P & f . s,C nin T implies [s,(if-then-else C,I,J)] in P ) & ( [s,C] in P & ex r being non empty FinSequence of S st
( r . 1 = f . s,C & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in P & r . (i + 1) = f . (r . i),(I \; C) ) ) ) implies [s,(while C,I)] in P ) ) ) holds
Y1 c= P ) & [:S,(ElementaryInstructions A):] c= Y2 & [:S,{(EmptyIns A)}:] c= Y2 & ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in Y2 & [(f . s,I),J] in Y2 implies [s,(I \; J)] in Y2 ) & ( [s,C] in Y2 & [(f . s,C),I] in Y2 & f . s,C in T implies [s,(if-then-else C,I,J)] in Y2 ) & ( [s,C] in Y2 & [(f . s,C),J] in Y2 & f . s,C nin T implies [s,(if-then-else C,I,J)] in Y2 ) & ( [s,C] in Y2 & ex r being non empty FinSequence of S st
( r . 1 = f . s,C & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in Y2 & r . (i + 1) = f . (r . i),(I \; C) ) ) ) implies [s,(while C,I)] in Y2 ) ) ) & ( for P being Subset of [:S,the carrier of A:] st [:S,(ElementaryInstructions A):] c= P & [:S,{(EmptyIns A)}:] c= P & ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in P & [(f . s,I),J] in P implies [s,(I \; J)] in P ) & ( [s,C] in P & [(f . s,C),I] in P & f . s,C in T implies [s,(if-then-else C,I,J)] in P ) & ( [s,C] in P & [(f . s,C),J] in P & f . s,C nin T implies [s,(if-then-else C,I,J)] in P ) & ( [s,C] in P & ex r being non empty FinSequence of S st
( r . 1 = f . s,C & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in P & r . (i + 1) = f . (r . i),(I \; C) ) ) ) implies [s,(while C,I)] in P ) ) ) holds
Y2 c= P ) implies Y1 = Y2 )
assume that
A9: S₁[Y1] and
A10: for Y being Subset of [:S,the carrier of A:] st S₁[Y] holds
Y1 c= Y and
A11: S₁[Y2] and
A12: for Y being Subset of [:S,the carrier of A:] st S₁[Y] holds
Y2 c= Y ; :: thesis: Y1 = Y2
thus Y1 c= Y2 by A11, A10; :: according to XBOOLE_0:def 10 :: thesis: Y2 c= Y1
thus Y2 c= Y1 by A9, A12; :: thesis: verum